coq - Easy way to simplify expression within anonymous function? -


assume need prove following:

x: nat  (fun _ : nat => 0) = (fun y : nat => if beq_nat x y 0 else 0)

since y not in environment, looks can't destruct on beq_nat x y simplify right-hand side. there simple way simplify expressions within anonymous function?

besides being able massage 2 functions equal, there way deduce 2 functions same showing produce same value on inputs?

edit: realize might asking impossible, since functions not same, it's when applied argument produce same value. i'm not sure how coq interprets this.

i believe case of referred functional extensionality, want prove 2 functions extensionally equal (they behave same caller's point of view).

you cannot prove directly in coq (since = definitioinal equality, not true), if wish to, can require module:

http://coq.inria.fr/stdlib/coq.logic.functionalextensionality.html

which provide axioms functional extensionality. can call tactic extensionality y. give access y.


Comments

Post a Comment

Popular posts from this blog

monitor web browser programmatically in Android? -

i've got tricky question here. need users make payment bank (namely barclaycard) in uk. so, have https url , add parameters (such amount pay, order reference, etc) url, start http connection intent.actionview, redirect user browser can enter credit card details on bank's webpage , make payment our account successfully. far ? the code use below (i changed values privacy reasons) problem is, need app when user has completed/failed/cancelled payment. barclaycardautomatically redirects particular url when payment has succeeded, 1 if failed. there no way of knowing when barclaycard payment has succeeded go android app somehow ? button cardbutton = (button) findviewbyid(r.id.card_button); cardbutton.setonclicklistener(new view.onclicklistener() { @override public void onclick(view arg0) { string prehashstring = new string(); string prohashstring = new string(); string shapassphrase = new string(); shapassphrase = "gsvth£h70zkh...
Read more

Shrink a YouTube video to responsive width -

i have youtube video embedded on our website , when shrink screen tablet or phone sizes stops shrinking @ around 560px in width. standard youtube videos or there can add code make go smaller? you can make youtube videos responsive css. wrap iframe in div class of "videowrapper" , apply following styles: .videowrapper { float: none; clear: both; width: 100%; position: relative; padding-bottom: 56.25%; padding-top: 25px; height: 0; } .videowrapper iframe { position: absolute; top: 0; left: 0; width: 100%; height: 100%; } the .videowrapper div should inside responsive element. padding on .videowrapper necessary keep video collapsing. may have tweak numbers depending upon layout.
Read more

wpf - PdfWriter.GetInstance throws System.NullReferenceException -

i'm trying create pdf document using itextsharp 5.3.4 using following document document = new document(); filestream stm = new filestream(filename, filemode.create); pdfwriter writer = pdfwriter.getinstance(document, stm); i'm getting system.nullreferenceexception following stack trace: system.nullreferenceexception occurred hresult=-2147467261 message=la référence d'objet n'est pas définie à une instance d'un objet. source=itextsharp stacktrace: à itextsharp.text.version.getinstance() innerexception: i've verified neither document nor stm null, , if select "continue" in vs12 document created - exception thrown. updated itextsharp 5.4.0 , it's still occurring. can't find information on anywhere - got ideas? make sure not catching exceptions. nullreferenceexception can 1 caught , handled inside itextsharp, don't care it. fact can continue supports theory. change following setting verify: debug -> exceptions ...
Read more