coq - Handling let in hypothesis -


as exercise in coq, i'm trying prove following function returns pair of lists of equal length.

require import list.  fixpoint split (a b:set)(x:list (a*b)) : (list a)*(list b) := match x |nil => (nil, nil) |cons (a,b) x1 => let (ta, tb) := split b x1 in (a::ta, b::tb) end.  theorem split_eq_len : forall (a b:set)(x:list (a*b))(y:list a)(z:list b),(split b x)=(y,z) -> length y = length z. proof. intros b x. elim x. simpl. intros y z. intros h. injection h. intros h1 h2. rewrite <- h1. rewrite <- h2. reflexivity. intros hx. elim hx. intros b tx h y z. simpl. intro.

after last step hypothesis let statement inside, not know how handle:

1 subgoals : set b : set x : list (a * b) hx : * b : b : b tx : list (a * b) h : forall (y : list a) (z : list b),     split b tx = (y, z) -> length y = length z y : list z : list b h0 : (let (ta, tb) := split b tx in (a :: ta, b :: tb)) = (y, z) ______________________________________(1/1) length y = length z

you want destruct (split b tx). break up, binding 2 pieces ta , tb


Comments

Post a Comment

Popular posts from this blog

powershell Start-Process exit code -1073741502 when used with Credential from a windows service environment -

i'm running strange behavior powershell start-process call. here call: $process = start-process ` "c:\somepath\mybinary.exe" ` -passthru ` -credential $defaultcredential ` -wait ` -workingdirectory "c:\somepath" ` -loaduserprofile if ($process.exitcode -ne 0) { #do } this call return exit code - 1073741502 . after quick search, exit code seems related generic error when program not load required dll (aka. status_dll_init_failed ). when run without -credential $credential program runs correctly. in order isolate problem, manually launched some.exe in prompt target credential , runs smoothly. so problem seems come way start-process cmdlet launch process. i found potential solutions problem tried apply no luck : link , link . would have idea of what's going on here ? edit 1: run proc mon monitoring program activities when launched directly or via powershell script. problem seems occur when loading kernelbase
Read more

twig - Using Twigbridge in a Laravel 5.1 Package -

i'm trying create laravel 5.1 package uses twigbridge instead of .php views. can normal .php views display fine, when try make use of .twig templates i'm met error. possible use twigbridge templates when creating views laravel package or pretty stuck blade , php ? edit 1: loading twig template without extending works. it's when start using {% extends 'file' %} error comes out. i error error loading /virtual/laravel/packages/username/mypackage/src/views/sample.twig: template "templates.master" not defined () in "/virtual/laravel/packages/username/mypackage/src/views/sample.twig" @ line 1. my folders username |_ mypackage |_ src |_ controllers - samplecontroller.php |_ views |_ templates - master.twig - sample.twig twig template sample.twig {% extends 'templates.master' %} {% block content %} {{ parent()
Read more

c# - LINQ join Entities from HashSet's, Join vs Dictionary vs HashSet performance -

i have hashset's each stores t, have written test application compares different relation algorithms can think of, i'm not pleased results getting. does there exist more efficient ways of achieving object relations, once testing? using system; using system.collections.generic; using system.linq; using system.text; using system.threading.tasks; using system.diagnostics; namespace linqtests { class program { static void main(string[] args) { hashset<user> usertable = new hashset<user>(); hashset<userproperty> userpropertytable = new hashset<userproperty>(); #region lets create dummy data. console.writeline("please wait while creating dummy data, can take while..."); console.writeline(""); int rows = 1000000; for(int x = 0; x < rows; x++) { random rnd = new random(); // ad
Read more