archive-nl.com » NL » R » ROBBERTKREBBERS.NL

Total: 145

Choose link from "Titles, links and description words view":

Or switch to "Titles and links view".
  • Module orders
    R x1 l1 x2 l2 if decide R x1 x2 then x1 list merge R l1 x2 l2 else x2 list merge R x1 l1 l2 Proof done Qed Lemma HdRel list merge x l1 l2 HdRel R x l1 HdRel R x l2 HdRel R x list merge R l1 l2 Proof destruct 1 as x1 l1 IH1 1 as x2 l2 IH2 rewrite list merge cons simpl repeat case decide auto Qed Lemma Sorted list merge l1 l2 Sorted R l1 Sorted R l2 Sorted R list merge R l1 l2 Proof intros Hl1 revert l2 induction Hl1 as x1 l1 IH1 induction 1 as x2 l2 IH2 rewrite list merge cons simpl repeat case decide constructor eauto using HdRel list merge HdRel cons total not Qed Lemma merge Permutation l1 l2 list merge R l1 l2 ₚ l1 l2 Proof revert l2 induction l1 as x1 l1 IH1 intros l2 induction l2 as x2 l2 IH2 rewrite list merge cons simpl repeat case decide auto by rewrite right id L by rewrite IH2 Permutation middle Qed Local Notation stack list option list A Inductive merge stack Sorted stack Prop merge stack Sorted nil merge stack Sorted merge stack Sorted cons None st merge stack Sorted st merge stack Sorted None st merge stack Sorted cons Some l st Sorted R l merge stack Sorted st merge stack Sorted Some l st Fixpoint merge stack flatten st stack list A match st with None st merge stack flatten st Some l st l merge stack flatten st end Lemma Sorted merge list to stack st l merge stack Sorted st Sorted R l merge stack Sorted merge list to stack R st l Proof intros Hst revert l induction Hst repeat constructor naive solver auto using Sorted list merge Qed Lemma merge list to stack Permutation st l merge stack flatten merge list to stack R st l ₚ l merge stack flatten st Proof revert l induction st as l st IH intros l simpl auto by rewrite IH merge Permutation associative L commutative l Qed Lemma Sorted merge stack st merge stack Sorted st Sorted R merge stack R st Proof induction 1 simpl auto using Sorted list merge Qed Lemma merge stack Permutation st merge stack R st ₚ merge stack flatten st Proof induction st as IH intros simpl auto by rewrite merge Permutation IH Qed Lemma Sorted merge sort aux st l merge stack Sorted st Sorted R merge sort aux R st l Proof revert st induction l simpl auto using Sorted merge stack Sorted merge list to stack Qed Lemma merge sort aux Permutation st l merge sort aux R st l ₚ merge stack flatten st l Proof revert st induction l as IH simpl intros by rewrite right id L merge stack Permutation rewrite IH merge list to stack Permutation simpl by rewrite Permutation middle Qed Lemma Sorted merge sort l Sorted R merge sort R l Proof apply Sorted merge sort aux by constructor Qed Lemma merge sort Permutation l merge sort R l ₚ l Proof unfold merge sort by rewrite merge sort aux Permutation Qed Lemma StronglySorted merge sort Transitive R l StronglySorted R merge sort R l Proof auto using Sorted StronglySorted Sorted merge sort Qed End merge sort correct Canonical pre and partial orders We extend the canonical pre order to a partial order by defining setoid equality as λ X Y X Y Y X We prove that this indeed gives rise to a setoid Instance preorder equiv SubsetEq A Equiv A λ X Y X Y Y X Section preorder Context SubsetEq A PreOrder subseteq A Instance preorder equivalence Equivalence A Proof split done by intros by intros X Y Z split transitivity Y Qed Global Instance Proper iff Proof unfold equiv preorder equiv intros X1 Y1 X2 Y2 split intro transitivity X1 tauto transitivity X2 tauto transitivity Y1 tauto transitivity Y2 tauto Qed Lemma subset spec X Y X Y X Y X Y Proof split intros HYX split done contradict HYX by rewrite HYX intros HXY split done by contradict HXY Qed Section dec Context X Y A Decision X Y Global Instance preorder equiv dec slow X Y A Decision X Y 100 Lemma subseteq inv X Y X Y X Y X Y Proof rewrite subset spec destruct decide X Y tauto Qed Lemma not subset inv X Y X Y X Y X Y Proof rewrite subset spec destruct decide X Y tauto Qed End dec Section leibniz Context LeibnizEquiv A Lemma subset spec L X Y X Y X Y X Y Proof unfold leibniz apply subset spec Qed Context X Y A Decision X Y Lemma subseteq inv L X Y X Y X Y X Y Proof unfold leibniz apply subseteq inv Qed Lemma not subset inv L X Y X Y X Y X Y Proof unfold leibniz apply not subset inv Qed End leibniz End preorder Typeclasses Opaque preorder equiv Hint Extern 0 Equivalence class apply preorder equivalence typeclass instances Partial orders Section partial order Context SubsetEq A PartialOrder subseteq A Global Instance LeibnizEquiv A Proof split intros by apply anti symmetric by intros Qed End partial order Join semi lattices General purpose theorems on join semi lattices Section join semi lattice Context Empty A JoinSemiLattice A EmptySpec A Implicit Types X Y A Implicit Types Xs Ys list A Hint Resolve subseteq empty union subseteq l union subseteq r union least Lemma union subseteq l transitive X1 X2 Y X1 X2 X1 X2 Y Proof intros transitivity X2 auto Qed Lemma union subseteq r transitive X1 X2 Y X1 X2 X1 Y X2 Proof intros transitivity X2 auto Qed Hint Resolve union subseteq l transitive union subseteq r transitive Lemma union preserving l X Y1 Y2 Y1 Y2 X Y1 X Y2 Proof auto Qed Lemma union preserving r X1 X2 Y X1 X2 X1 Y X2 Y Proof auto Qed

    Original URL path: http://robbertkrebbers.nl/research/ch2o/orders.html (2015-08-10)
    Open archived version from archive


  • Module option
    mbind g f Proof by destruct x simpl Qed Lemma option bind ext A B f g A option B x y a f a g a x y x f y g Proof intros destruct x y simplify equality csimpl auto Qed Lemma option bind ext fun A B f g A option B x a f a g a x f x g Proof intros by apply option bind ext Qed Lemma bind Some A B f A option B x option A b x f Some b a x Some a f a Some b Proof split by destruct x as a exists a by intros Qed Lemma bind None A B f A option B x option A x f None x None a x Some a f a None Proof split by intros destruct x intros simplify equality eauto Qed Lemma bind with Some A x option A x Some x Proof by destruct x Qed Inverses of constructors We can do this in a fancy way using dependent types but rewrite does not particularly like type level reductions Class Maybe A B Type c A B maybe B option A Arguments maybe Class Maybe2 A1 A2 B Type c A1 A2 B maybe2 B option A1 A2 Arguments maybe2 Class Maybe3 A1 A2 A3 B Type c A1 A2 A3 B maybe3 B option A1 A2 A3 Arguments maybe3 Class Maybe4 A1 A2 A3 A4 B Type c A1 A2 A3 A4 B maybe4 B option A1 A2 A3 A4 Arguments maybe4 Instance maybe comp Maybe B C c1 Maybe A B c2 Maybe c1 c2 λ x maybe c1 x maybe c2 Arguments maybe comp Instance maybe inl A B Maybe inl A B λ xy match xy with inl x Some x None end Instance maybe inr A B Maybe inr A B λ xy match xy with inr y Some y None end Instance maybe Some A Maybe Some A id Arguments maybe Some Union intersection and difference Instance option union with A UnionWith A option A λ f x y match x y with Some a Some b f a b Some a None Some a None Some b Some b None None None end Instance option intersection with A IntersectionWith A option A λ f x y match x y with Some a Some b f a b None end Instance option difference with A DifferenceWith A option A λ f x y match x y with Some a Some b f a b Some a None Some a None None end Instance option union A Union option A union with λ x Some x Lemma option union Some A x y option A z x y Some z x Some z y Some z Proof destruct x y intros simplify equality auto Qed Section option union intersection difference Context A f A A option A Global Instance LeftId None union with f Proof by intros Qed Global Instance

    Original URL path: http://robbertkrebbers.nl/research/ch2o/option.html (2015-08-10)
    Open archived version from archive

  • Module error
    destruct x s as naive solver Qed Lemma error fmap ret S E A B f A B s s x error S E A b f x s mret b s a x s mret a s b f a Proof compute destruct x s as naive solver Qed Lemma error of option ret S E A s s S o option A e E a error of option o e s mret a s o Some a s s Proof compute destruct o naive solver Qed Lemma error guard ret S E A dec Decision P s s x error S E A e a guard P with e x s mret a s P x s mret a s Proof compute destruct dec naive solver Qed Lemma error fmap bind S E A B C f A B g B error S E C x s f x g s x g f s Proof by compute destruct x s as Qed Lemma error associative S E A B C f A error S E B g B error S E C x s x f g s a x f a g s Proof by compute destruct x s as Qed Lemma error of option bind S E A B f A option B o e error of option S S E E o f e a error of option o e error of option f a e Proof by destruct o Qed Lemma error gets spec S E A g S A s gets E E g s mret g s s Proof done Qed Lemma error modify spec S E g S S s modify E E g s mret g s Proof done Qed Lemma error left gets S E A B g S A f A error S E B s gets E E g f s f g s s Proof done Qed Lemma error left modify S E B g S S f unit error S E B s modify E E g f s f g s Proof done Qed Lemma error left id S E A B a A f A error S E B mret a f f a Proof done Qed Ltac generalize errors csimpl let gen error e try is var e fail 1 generalize e let x fresh err in intros x in repeat match goal with appcontext fail e gen error e appcontext error guard e gen error e appcontext error of option e gen error e end Tactic Notation simplify error equality repeat match goal with H context gets rewrite error gets spec in H H context modify rewrite error modify spec in H H mret M error rewrite error left id in H H gets rewrite error left gets in H H modify rewrite error left modify in H H error guard apply error guard ret in H destruct H progress simplify equality H error of option apply error of option

    Original URL path: http://robbertkrebbers.nl/research/ch2o/error.html (2015-08-10)
    Open archived version from archive

  • Module list
    singleton l x l ₚ x l x Proof split by intro apply Permutation length 1 inv by intros Qed Definition Permutation skip perm skip A Definition Permutation swap perm swap A Definition Permutation singleton inj Permutation length 1 A Global Existing Instance Permutation app Proper Global Instance Proper ₚ length A Proof induction 1 simpl auto with lia Qed Global Instance Commutative ₚ app A Proof intros l1 induction l1 as x l1 IH intros l2 simpl by rewrite right id L rewrite Permutation middle IH simpl by rewrite Permutation middle Qed Global Instance x A Injective ₚ ₚ x Proof red eauto using Permutation cons inv Qed Global Instance k list A Injective ₚ ₚ k Proof red induction k as x k IH intros l1 l2 simpl auto intros by apply IH injective x Qed Global Instance k list A Injective ₚ ₚ k Proof intros k l1 l2 rewrite commutative k by apply injective k Qed Lemma replicate Permutation n x l replicate n x ₚ l replicate n x l Proof intros Hl apply replicate as elem of split by rewrite Hl replicate length intros y rewrite Hl by apply elem of replicate inv Qed Lemma reverse Permutation l reverse l ₚ l Proof induction l as x l IH done by rewrite reverse cons commutative IH Qed Properties of the prefix of and suffix of predicates Global Instance PreOrder prefix of A Proof split intros eexists by rewrite right id L intros k1 k2 exists k1 k2 by rewrite associative L Qed Lemma prefix of nil l prefix of l Proof by exists l Qed Lemma prefix of nil not x l x l prefix of Proof by intros k Qed Lemma prefix of cons x l1 l2 l1 prefix of l2 x l1 prefix of x l2 Proof intros k by exists k Qed Lemma prefix of cons alt x y l1 l2 x y l1 prefix of l2 x l1 prefix of y l2 Proof intros apply prefix of cons Qed Lemma prefix of cons inv 1 x y l1 l2 x l1 prefix of y l2 x y Proof by intros k simplify equality Qed Lemma prefix of cons inv 2 x y l1 l2 x l1 prefix of y l2 l1 prefix of l2 Proof intros k simplify equality by exists k Qed Lemma prefix of app k l1 l2 l1 prefix of l2 k l1 prefix of k l2 Proof intros k exists k by rewrite associative L Qed Lemma prefix of app alt k1 k2 l1 l2 k1 k2 l1 prefix of l2 k1 l1 prefix of k2 l2 Proof intros apply prefix of app Qed Lemma prefix of app l l1 l2 l3 l1 l3 prefix of l2 l1 prefix of l2 Proof intros k exists l3 k by rewrite associative L Qed Lemma prefix of app r l1 l2 l3 l1 prefix of l2 l1 prefix of l2 l3 Proof intros k exists k l3 by rewrite associative L Qed Lemma prefix of length l1 l2 l1 prefix of l2 length l1 length l2 Proof intros rewrite app length lia Qed Lemma prefix of snoc not l x l x prefix of l Proof intros discriminate list equality Qed Global Instance PreOrder suffix of A Proof split intros by eexists intros k1 k2 exists k2 k1 by rewrite associative L Qed Global Instance prefix of dec x y Decision x y l1 l2 Decision l1 prefix of l2 fix go l1 l2 match l1 l2 return l1 prefix of l2 l1 prefix of l2 with left prefix of nil right prefix of nil not x l1 y l2 match decide rel x y with left Hxy match go l1 l2 with left Hl1l2 left prefix of cons alt Hxy Hl1l2 right Hl1l2 right Hl1l2 prefix of cons inv 2 end right Hxy right Hxy prefix of cons inv 1 end end Section prefix ops Context x y Decision x y Lemma max prefix of fst l1 l2 l1 max prefix of l1 l2 2 max prefix of l1 l2 1 1 Proof revert l2 induction l1 intros simpl repeat case decide f equal auto Qed Lemma max prefix of fst alt l1 l2 k1 k2 k3 max prefix of l1 l2 k1 k2 k3 l1 k3 k1 Proof intros pose proof max prefix of fst l1 l2 by destruct max prefix of l1 l2 as simplify equality Qed Lemma max prefix of fst prefix l1 l2 max prefix of l1 l2 2 prefix of l1 Proof eexists apply max prefix of fst Qed Lemma max prefix of fst prefix alt l1 l2 k1 k2 k3 max prefix of l1 l2 k1 k2 k3 k3 prefix of l1 Proof eexists eauto using max prefix of fst alt Qed Lemma max prefix of snd l1 l2 l2 max prefix of l1 l2 2 max prefix of l1 l2 1 2 Proof revert l2 induction l1 intros simpl repeat case decide f equal auto Qed Lemma max prefix of snd alt l1 l2 k1 k2 k3 max prefix of l1 l2 k1 k2 k3 l2 k3 k2 Proof intro pose proof max prefix of snd l1 l2 by destruct max prefix of l1 l2 as simplify equality Qed Lemma max prefix of snd prefix l1 l2 max prefix of l1 l2 2 prefix of l2 Proof eexists apply max prefix of snd Qed Lemma max prefix of snd prefix alt l1 l2 k1 k2 k3 max prefix of l1 l2 k1 k2 k3 k3 prefix of l2 Proof eexists eauto using max prefix of snd alt Qed Lemma max prefix of max l1 l2 k k prefix of l1 k prefix of l2 k prefix of max prefix of l1 l2 2 Proof intros l1 l2 by induction k simpl repeat case decide simpl auto using prefix of nil prefix of cons Qed Lemma max prefix of max alt l1 l2 k1 k2 k3 k max prefix of l1 l2 k1 k2 k3 k prefix of l1 k prefix of l2 k prefix of k3 Proof intro pose proof max prefix of max l1 l2 k by destruct max prefix of l1 l2 as simplify equality Qed Lemma max prefix of max snoc l1 l2 k1 k2 k3 x1 x2 max prefix of l1 l2 x1 k1 x2 k2 k3 x1 x2 Proof intros Hl destruct prefix of snoc not k3 x2 eapply max prefix of max alt eauto rewrite max prefix of fst alt Hl apply prefix of app prefix of cons prefix of nil rewrite max prefix of snd alt Hl apply prefix of app prefix of cons prefix of nil Qed End prefix ops Lemma prefix suffix reverse l1 l2 l1 prefix of l2 reverse l1 suffix of reverse l2 Proof split intros k E exists reverse k by rewrite E reverse app by rewrite reverse involutive l2 E reverse app reverse involutive Qed Lemma suffix prefix reverse l1 l2 l1 suffix of l2 reverse l1 prefix of reverse l2 Proof by rewrite prefix suffix reverse reverse involutive Qed Lemma suffix of nil l suffix of l Proof exists l by rewrite right id L Qed Lemma suffix of nil inv l l suffix of l Proof by intros simplify list equality Qed Lemma suffix of cons nil inv x l x l suffix of Proof by intros Qed Lemma suffix of snoc l1 l2 x l1 suffix of l2 l1 x suffix of l2 x Proof intros k exists k by rewrite associative L Qed Lemma suffix of snoc alt x y l1 l2 x y l1 suffix of l2 l1 x suffix of l2 y Proof intros apply suffix of snoc Qed Lemma suffix of app l1 l2 k l1 suffix of l2 l1 k suffix of l2 k Proof intros k exists k by rewrite associative L Qed Lemma suffix of app alt l1 l2 k1 k2 k1 k2 l1 suffix of l2 l1 k1 suffix of l2 k2 Proof intros apply suffix of app Qed Lemma suffix of snoc inv 1 x y l1 l2 l1 x suffix of l2 y x y Proof intros k E rewrite associative L in E by simplify list equality Qed Lemma suffix of snoc inv 2 x y l1 l2 l1 x suffix of l2 y l1 suffix of l2 Proof intros k E exists k rewrite associative L in E by simplify list equality Qed Lemma suffix of app inv l1 l2 k l1 k suffix of l2 k l1 suffix of l2 Proof intros k E exists k rewrite associative L in E by simplify list equality Qed Lemma suffix of cons l l1 l2 x x l1 suffix of l2 l1 suffix of l2 Proof intros k exists k x by rewrite associative L Qed Lemma suffix of app l l1 l2 l3 l3 l1 suffix of l2 l1 suffix of l2 Proof intros k exists k l3 by rewrite associative L Qed Lemma suffix of cons r l1 l2 x l1 suffix of l2 l1 suffix of x l2 Proof intros k by exists x k Qed Lemma suffix of app r l1 l2 l3 l1 suffix of l2 l1 suffix of l3 l2 Proof intros k exists l3 k by rewrite associative L Qed Lemma suffix of cons inv l1 l2 x y x l1 suffix of y l2 x l1 y l2 x l1 suffix of l2 Proof intros k E by left right simplify equality by apply suffix of app r Qed Lemma suffix of length l1 l2 l1 suffix of l2 length l1 length l2 Proof intros rewrite app length lia Qed Lemma suffix of cons not x l x l suffix of l Proof intros discriminate list equality Qed Global Instance suffix of dec x y Decision x y l1 l2 Decision l1 suffix of l2 Proof refine cast if decide rel prefix of reverse l1 reverse l2 abstract by rewrite suffix prefix reverse Defined Section max suffix of Context x y Decision x y Lemma max suffix of fst l1 l2 l1 max suffix of l1 l2 1 1 max suffix of l1 l2 2 Proof rewrite reverse involutive l1 at 1 rewrite max prefix of fst reverse l1 reverse l2 unfold max suffix of destruct max prefix of reverse l1 reverse l2 as simpl by rewrite reverse app Qed Lemma max suffix of fst alt l1 l2 k1 k2 k3 max suffix of l1 l2 k1 k2 k3 l1 k1 k3 Proof intro pose proof max suffix of fst l1 l2 by destruct max suffix of l1 l2 as simplify equality Qed Lemma max suffix of fst suffix l1 l2 max suffix of l1 l2 2 suffix of l1 Proof eexists apply max suffix of fst Qed Lemma max suffix of fst suffix alt l1 l2 k1 k2 k3 max suffix of l1 l2 k1 k2 k3 k3 suffix of l1 Proof eexists eauto using max suffix of fst alt Qed Lemma max suffix of snd l1 l2 l2 max suffix of l1 l2 1 2 max suffix of l1 l2 2 Proof rewrite reverse involutive l2 at 1 rewrite max prefix of snd reverse l1 reverse l2 unfold max suffix of destruct max prefix of reverse l1 reverse l2 as simpl by rewrite reverse app Qed Lemma max suffix of snd alt l1 l2 k1 k2 k3 max suffix of l1 l2 k1 k2 k3 l2 k2 k3 Proof intro pose proof max suffix of snd l1 l2 by destruct max suffix of l1 l2 as simplify equality Qed Lemma max suffix of snd suffix l1 l2 max suffix of l1 l2 2 suffix of l2 Proof eexists apply max suffix of snd Qed Lemma max suffix of snd suffix alt l1 l2 k1 k2 k3 max suffix of l1 l2 k1 k2 k3 k3 suffix of l2 Proof eexists eauto using max suffix of snd alt Qed Lemma max suffix of max l1 l2 k k suffix of l1 k suffix of l2 k suffix of max suffix of l1 l2 2 Proof generalize max prefix of max reverse l1 reverse l2 rewrite suffix prefix reverse unfold max suffix of destruct max prefix of reverse l1 reverse l2 as simpl rewrite reverse involutive auto Qed Lemma max suffix of max alt l1 l2 k1 k2 k3 k max suffix of l1 l2 k1 k2 k3 k suffix of l1 k suffix of l2 k suffix of k3 Proof intro pose proof max suffix of max l1 l2 k by destruct max suffix of l1 l2 as simplify equality Qed Lemma max suffix of max snoc l1 l2 k1 k2 k3 x1 x2 max suffix of l1 l2 k1 x1 k2 x2 k3 x1 x2 Proof intros Hl destruct suffix of cons not x2 k3 eapply max suffix of max alt eauto rewrite max suffix of fst alt Hl by apply suffix of app x2 suffix of app r rewrite max suffix of snd alt Hl by apply suffix of app x2 suffix of app r Qed End max suffix of Properties of the sublist predicate Lemma sublist length l1 l2 l1 sublist l2 length l1 length l2 Proof induction 1 simpl auto with arith Qed Lemma sublist nil l l sublist l Proof induction l try constructor auto Qed Lemma sublist nil r l l sublist l Proof split by inversion 1 intros constructor Qed Lemma sublist app l1 l2 k1 k2 l1 sublist l2 k1 sublist k2 l1 k1 sublist l2 k2 Proof induction 1 simpl try constructor auto Qed Lemma sublist inserts l k l1 l2 l1 sublist l2 l1 sublist k l2 Proof induction k try constructor auto Qed Lemma sublist inserts r k l1 l2 l1 sublist l2 l1 sublist l2 k Proof induction 1 simpl try constructor auto using sublist nil l Qed Lemma sublist cons r x l k l sublist x k l sublist k l l x l l sublist k Proof split inversion 1 eauto intros constructor auto Qed Lemma sublist cons l x l k x l sublist k k1 k2 k k1 x k2 l sublist k2 Proof split intros Hlk induction k as y k IH inversion Hlk eexists k by repeat constructor destruct IH as k1 k2 auto by exists y k1 k2 intros k1 k2 by apply sublist inserts l sublist skip Qed Lemma sublist app r l k1 k2 l sublist k1 k2 l1 l2 l l1 l2 l1 sublist k1 l2 sublist k2 Proof split revert l k2 induction k1 as y k1 IH intros l k2 simpl eexists l by repeat constructor rewrite sublist cons r intros l subst destruct IH l k2 as l1 l2 trivial subst exists l1 l2 auto using sublist cons destruct IH l k2 as l1 l2 trivial subst exists y l1 l2 auto using sublist skip intros subst auto using sublist app Qed Lemma sublist app l l1 l2 k l1 l2 sublist k k1 k2 k k1 k2 l1 sublist k1 l2 sublist k2 Proof split revert l2 k induction l1 as x l1 IH intros l2 k simpl eexists k by repeat constructor rewrite sublist cons l intros k1 k2 subst destruct IH l2 k2 as h1 h2 trivial subst exists k1 x h1 h2 rewrite associative L auto using sublist inserts l sublist skip intros subst auto using sublist app Qed Lemma sublist app inv l k l1 l2 k l1 sublist k l2 l1 sublist l2 Proof induction k as y k IH simpl done rewrite sublist cons r intros Hl12 simplify equality eauto rewrite sublist cons l in Hl12 destruct Hl12 as k1 k2 Hk apply IH rewrite Hk eauto using sublist inserts l sublist cons Qed Lemma sublist app inv r k l1 l2 l1 k sublist l2 k l1 sublist l2 Proof revert l1 l2 induction k as y k IH intros l1 l2 by rewrite right id L intros feed pose proof IH l1 y l2 y as Hl12 by rewrite associative L rewrite sublist app l in Hl12 destruct Hl12 as k1 k2 E Hk2 destruct k2 as z k2 using rev ind inversion Hk2 rewrite associative L in E simplify list equality eauto using sublist inserts r Qed Global Instance PartialOrder sublist A Proof split split intros l induction l constructor auto intros l1 l2 l3 Hl12 revert l3 induction Hl12 auto using sublist nil l intros rewrite sublist cons l intros subst eauto using sublist inserts l sublist skip intros rewrite sublist cons l intros subst eauto using sublist inserts l sublist cons intros l1 l2 Hl12 Hl21 apply sublist length in Hl21 induction Hl12 f equal auto with arith apply sublist length in Hl12 lia Qed Lemma sublist take l i take i l sublist l Proof rewrite take drop i l at 2 by apply sublist inserts r Qed Lemma sublist drop l i drop i l sublist l Proof rewrite take drop i l at 2 by apply sublist inserts l Qed Lemma sublist delete l i delete i l sublist l Proof revert i by induction l intros simpl constructor Qed Lemma sublist foldr delete l is foldr delete l is sublist l Proof induction is as i is IH simpl done transitivity foldr delete l is auto using sublist delete Qed Lemma sublist alt l1 l2 l1 sublist l2 is l1 foldr delete l2 is Proof split intros is apply sublist foldr delete intros Hl12 cut k is k l1 foldr delete k l2 is intros help apply help induction Hl12 as x l1 l2 IH x l1 l2 IH intros k by eexists destruct IH k x as is His exists is by rewrite associative L in His destruct IH k as is His exists is length k rewrite fold right app simpl by rewrite delete middle Qed Lemma Permutation sublist l1 l2 l3 l1 ₚ l2 l2 sublist l3 l4 l1 sublist l4 l4 ₚ l3 Proof intros Hl1l2 revert l3 induction Hl1l2 as x l1 l2 IH x y l1 l1 l1 l2 IH1 IH2 intros l3 by exists l3 intros l3 rewrite sublist cons l intros l3 l3 subst destruct IH l3 as l4 Hl4 auto exists l3 x l4 split by apply sublist inserts l sublist skip by rewrite Hl4 intros l3 rewrite sublist cons l intros l3 l3 Hl3 subst rewrite sublist cons l in Hl3 destruct Hl3 as l5 l5 Hl5 subst exists l3 y l5 x l5 split by do 2 apply sublist inserts l sublist skip by rewrite Permutation middle Permutation swap intros l3 destruct IH2 l3 as l3 trivial destruct IH1 l3 as l3 trivial exists l3 split done etransitivity eauto Qed Lemma sublist Permutation l1 l2 l3 l1 sublist l2 l2 ₚ l3 l4 l1 ₚ l4 l4 sublist l3 Proof intros Hl1l2 Hl2l3 revert l1 Hl1l2 induction Hl2l3 as x l2 l3 IH x y l2 l2 l2 l3 IH1 IH2 intros l1 by exists l1 intros l1 rewrite sublist cons r intros l1 l1 subst destruct IH l1 as l4 trivial exists l4 split done by constructor destruct IH l1 as l4 Hl4 auto exists x l4 split by constructor by constructor intros l1 rewrite sublist cons r intros Hl1 l1 l1 Hl1 subst exists l1 split done rewrite sublist cons r in Hl1 destruct Hl1 as l1 subst by repeat constructor rewrite sublist cons r in Hl1 destruct Hl1 as l1 subst exists y l1 by repeat constructor exists x y l1 by repeat constructor intros l1 destruct IH1 l1 as l3 trivial destruct IH2 l3 as l3 trivial exists l3 split done etransitivity eauto Qed Properties of the contains predicate Lemma contains length l1 l2 l1 contains l2 length l1 length l2 Proof induction 1 simpl auto with lia Qed Lemma contains nil l l contains l Proof induction l constructor auto Qed Lemma contains nil r l l contains l Proof split intros constructor intros Hl apply contains length in Hl destruct l simpl in auto with lia Qed Global Instance PreOrder contains A Proof split intros l induction l constructor auto red apply contains trans Qed Lemma Permutation contains l1 l2 l1 ₚ l2 l1 contains l2 Proof induction 1 econstructor eauto Qed Lemma sublist contains l1 l2 l1 sublist l2 l1 contains l2 Proof induction 1 constructor auto Qed Lemma contains Permutation l1 l2 l1 contains l2 k l2 ₚ l1 k Proof induction 1 as x y l k Hk x l1 l2 k Hk l1 l2 l3 k Hk k Hk by eexists exists k by rewrite Hk eexists rewrite right id L by constructor exists x k by rewrite Hk Permutation middle exists k k by rewrite Hk Hk associative L Qed Lemma contains Permutation length le l1 l2 length l2 length l1 l1 contains l2 l1 ₚ l2 Proof intros Hl21 Hl12 destruct contains Permutation l1 l2 as Hk auto by rewrite Hk right id L rewrite Hk app length in Hl21 simpl in Hl21 lia Qed Lemma contains Permutation length eq l1 l2 length l2 length l1 l1 contains l2 l1 ₚ l2 Proof intro apply contains Permutation length le lia Qed Global Instance Proper ₚ ₚ iff contains A Proof intros l1 l2 k1 k2 split intros transitivity l1 by apply Permutation contains transitivity k1 done by apply Permutation contains transitivity l2 by apply Permutation contains transitivity k2 done by apply Permutation contains Qed Global Instance AntiSymmetric ₚ contains A Proof red auto using contains Permutation length le contains length Qed Lemma contains take l i take i l contains l Proof auto using sublist take sublist contains Qed Lemma contains drop l i drop i l contains l Proof auto using sublist drop sublist contains Qed Lemma contains delete l i delete i l contains l Proof auto using sublist delete sublist contains Qed Lemma contains foldr delete l is foldr delete l is sublist l Proof auto using sublist foldr delete sublist contains Qed Lemma contains sublist l l1 l3 l1 contains l3 l2 l1 sublist l2 l2 ₚ l3 Proof split intros Hl13 elim Hl13 clear l1 l3 Hl13 by eexists intros x l1 l3 l2 exists x l2 by repeat constructor intros x y l exists y x l by repeat constructor intros x l1 l3 l2 exists x l2 by repeat constructor intros l1 l3 l5 l2 l4 destruct Permutation sublist l2 l3 l4 as l3 trivial exists l3 split etransitivity eauto intros l2 transitivity l2 auto using sublist contains Permutation contains Qed Lemma contains sublist r l1 l3 l1 contains l3 l2 l1 ₚ l2 l2 sublist l3 Proof rewrite contains sublist l split intros l2 eauto using sublist Permutation Permutation sublist Qed Lemma contains inserts l k l1 l2 l1 contains l2 l1 contains k l2 Proof induction k try constructor auto Qed Lemma contains inserts r k l1 l2 l1 contains l2 l1 contains l2 k Proof rewrite commutative apply contains inserts l Qed Lemma contains skips l k l1 l2 l1 contains l2 k l1 contains k l2 Proof induction k try constructor auto Qed Lemma contains skips r k l1 l2 l1 contains l2 l1 k contains l2 k Proof rewrite commutative k apply contains skips l Qed Lemma contains app l1 l2 k1 k2 l1 contains l2 k1 contains k2 l1 k1 contains l2 k2 Proof transitivity l1 k2 auto using contains skips l contains skips r Qed Lemma contains cons r x l k l contains x k l contains k l l ₚ x l l contains k Proof split rewrite contains sublist r intros l E Hl rewrite sublist cons r in Hl destruct Hl as subst left rewrite E eauto using sublist contains right eauto using sublist contains intros E rewrite E by constructor Qed Lemma contains cons l x l k x l contains k k k ₚ x k l contains k Proof split rewrite contains sublist l intros l Hl E rewrite sublist cons l in Hl destruct Hl as k1 k2 subst exists k1 k2 split eauto using contains inserts l sublist contains by rewrite Permutation middle intros E rewrite E by constructor Qed Lemma contains app r l k1 k2 l contains k1 k2 l1 l2 l ₚ l1 l2 l1 contains k1 l2 contains k2 Proof split rewrite contains sublist r intros l E Hl rewrite sublist app r in Hl destruct Hl as l1 l2 subst exists l1 l2 eauto using sublist contains intros E rewrite E eauto using contains app Qed Lemma contains app l l1 l2 k l1 l2 contains k k1 k2 k ₚ k1 k2 l1 contains k1 l2 contains k2 Proof split rewrite contains sublist l intros l Hl E rewrite sublist app l in Hl destruct Hl as k1 k2 subst exists k1 k2 split done eauto using sublist contains intros E rewrite E eauto using contains app Qed Lemma contains app inv l l1 l2 k k l1 contains k l2 l1 contains l2 Proof induction k as y k IH simpl done rewrite contains cons l intros E apply Permutation cons inv in E apply IH by rewrite E Qed Lemma contains app inv r l1 l2 k l1 k contains l2 k l1 contains l2 Proof revert l1 l2 induction k as y k IH intros l1 l2 by rewrite right id L intros feed pose proof IH l1 y l2 y as Hl12 by rewrite associative L rewrite contains app l in Hl12 destruct Hl12 as k1 k2 E1 Hk2 rewrite contains cons l in Hk2 destruct Hk2 as k2 E2 rewrite E2 Permutation cons append k2 associative L in E1 apply Permutation app inv r in E1 rewrite E1 eauto using contains inserts r Qed Lemma contains cons middle x l k1 k2 l contains k1 k2 x l contains k1 x k2 Proof rewrite Permutation middle by apply contains skip Qed Lemma contains app middle l1 l2 k1 k2 l2 contains k1 k2 l1 l2 contains k1 l1 k2 Proof rewrite associative commutative k1 l1 associative L by apply contains skips l Qed Lemma contains middle l k1 k2 l contains k1 l k2 Proof by apply contains inserts l contains inserts r Qed Lemma Permutation alt l1 l2 l1 ₚ l2 length l1 length l2 l1 contains l2 Proof split by intros Hl rewrite Hl intros auto using contains Permutation length eq Qed Lemma NoDup contains l k NoDup l x x l x k l contains k Proof intros Hl revert k induction Hl as x l Hx IH intros k Hk by apply contains nil l intros k Hlk destruct elem of list split k x as l1 l2 subst apply Hlk by constructor rewrite Permutation middle apply contains skip IH intros y Hy rewrite elem of app specialize Hlk y rewrite elem of app elem of cons in Hlk by destruct Hlk as subst eauto Qed Lemma NoDup Permutation l k NoDup l NoDup k x x l x k l ₚ k Proof intros apply anti symmetric contains apply NoDup contains naive solver Qed Section contains dec Context x y Decision x y Lemma list remove Permutation l1 l2 k1 x l1 ₚ l2 list remove x l1 Some k1 k2 list remove x l2 Some k2 k1 ₚ k2 Proof intros Hl revert k1 induction Hl as y l1 l2 IH y1 y2 l l1 l2 l3 IH1 IH2 simpl intros k1 Hk1 done case decide simplify equality eauto destruct list remove x l1 as l eqn simplify equality destruct IH l as simplify option equality eauto simplify option equality eauto using Permutation swap destruct IH1 k1 as k2 trivial destruct IH2 k2 as k3 trivial exists k3 split eauto by transitivity k2 Qed Lemma list remove Some l k x list remove x l Some k l ₚ x k Proof revert k induction l as y l IH simpl intros k done simplify option equality auto by rewrite Permutation swap IH Qed Lemma list remove Some inv l k x l ₚ x k k list remove x l Some k k ₚ k Proof intros destruct list remove Permutation x k l k x as k done simpl by case decide by exists k Qed Lemma list remove list contains l1 l2 l1 contains l2 is Some list remove list l1 l2 Proof split revert l2 induction l1 as x l1 IH simpl intros l2 by exists l2 intros l2 rewrite contains cons l intros k Hk destruct list remove Some inv l2 k x as k2 Hk2 trivial simplify option equality apply IH by rewrite Hk2 intros k Hk revert l2 k Hk induction l1 as x l1 IH simpl intros l2 k intros apply contains nil l destruct list remove x l2 as k eqn intros simplify equality rewrite contains cons l eauto using list remove Some Qed Global Instance contains dec l1 l2 Decision l1 contains l2 Proof refine cast if decide is Some list remove list l1 l2 abstract rewrite list remove list contains tauto Defined Global Instance Permutation dec l1 l2 Decision l1 ₚ l2 Proof refine cast if and decide length l1 length l2 decide l1 contains l2 abstract rewrite Permutation alt tauto Defined End contains dec End more general properties Properties of the Forall and Exists predicate Lemma Forall Exists dec A P Q A Prop dec x P x Q x l Forall P l Exists Q l Proof refine fix go l match l return Forall P l Exists Q l with left x l cast if and dec x go l end clear go intuition Defined Section Forall Exists Context A P A Prop Definition Forall nil 2 Forall nil A Definition Forall cons 2 Forall cons A Lemma Forall forall l Forall P l x x l P x Proof split induction 1 inversion 1 subst auto intros Hin induction l as x l IH constructor apply Hin constructor apply IH intros apply Hin by constructor Qed Lemma Forall nil Forall P True Proof done Qed Lemma Forall cons 1 x l Forall P x l P x Forall P l Proof by inversion 1 Qed Lemma Forall cons x l Forall P x l P x Forall P l Proof split by inversion 1 intros by constructor Qed Lemma Forall singleton x Forall P x P x Proof rewrite Forall cons Forall nil tauto Qed Lemma Forall app 2 l1 l2 Forall P l1 Forall P l2 Forall P l1 l2 Proof induction 1 simpl auto Qed Lemma Forall app l1 l2 Forall P l1 l2 Forall P l1 Forall P l2 Proof split induction l1 inversion 1 intuition intros auto using Forall app 2 Qed Lemma Forall true l x P x Forall P l Proof induction l auto Qed Lemma Forall impl Q A Prop l Forall P l x P x Q x Forall Q l Proof intros H induction H auto Defined Global Instance Forall proper Proper pointwise relation Forall A Proof split subst induction 1 constructor by firstorder auto Qed Lemma Forall iff l Q A Prop x P x Q x Forall P l Forall Q l Proof intros H apply Forall proper red apply H done Qed Lemma Forall not l length l 0 Forall not P l Forall P l Proof by destruct 2 inversion 1 Qed Lemma Forall and Q l Forall λ x P x Q x l Forall P l Forall Q l Proof split induction 1 constructor naive solver intros Hl Hl revert Hl induction Hl inversion clear 1 auto Qed Lemma Forall and l Q l Forall λ x P x Q x l Forall P l Proof rewrite Forall and tauto Qed Lemma Forall and r Q l Forall λ x P x Q x l Forall Q l Proof rewrite Forall and tauto Qed Lemma Forall delete l i Forall P l Forall P delete i l Proof intros H revert i by induction H intros i try constructor Qed Lemma Forall lookup l Forall P l i x l i Some x P x Proof rewrite Forall forall setoid rewrite elem of list lookup naive solver Qed Lemma Forall lookup 1 l i x Forall P l l i Some x P x Proof rewrite Forall lookup eauto Qed Lemma Forall lookup 2 l i x l i Some x P x Forall P l Proof by rewrite Forall lookup Qed Lemma Forall tail l Forall P l Forall P tail l Proof destruct 1 simpl auto Qed Lemma Forall alter f l i Forall P l x l i Some x P x P f x Forall P alter f i l Proof intros Hl revert i induction Hl simpl intros i constructor auto Qed Lemma Forall alter inv f l i Forall P alter f i l x l i Some x P f x P x Forall P l Proof revert i induction l intros simpl inversion clear 1 constructor eauto Qed Lemma Forall insert l i x Forall P l P x Forall P i x l Proof rewrite list insert alter auto using Forall alter Qed Lemma Forall inserts l i k Forall P l Forall P k Forall P list inserts i k l Proof intros Hl Hk revert i induction Hk simpl auto using Forall insert Qed Lemma Forall replicate n x P x Forall P replicate n x Proof induction n simpl constructor auto Qed Lemma Forall replicate eq n x A Forall x replicate n x Proof induction n simpl constructor auto Qed Lemma Forall take n l Forall P l Forall P take n l Proof intros Hl revert n induction Hl intros simpl auto Qed Lemma Forall drop n l Forall P l Forall P drop n l Proof intros Hl revert n induction Hl intros simpl auto Qed Lemma Forall resize n x l P x Forall P l Forall P resize n x l Proof intros Hl revert n induction Hl intros simpl auto using Forall replicate Qed Lemma Forall resize inv n x l length l n Forall P resize n x l Forall P l Proof intros rewrite resize ge Forall app by done by intros Qed Lemma Forall sublist lookup l i n k sublist lookup i n l Some k Forall P l Forall P k Proof unfold sublist lookup intros simplify option equality auto using Forall take Forall drop Qed Lemma Forall sublist alter f l i n k Forall P l sublist lookup i n l Some k Forall P f k Forall P sublist alter f i n l Proof unfold sublist alter sublist lookup intros simplify option equality auto using Forall app 2 Forall drop Forall take Qed Lemma Forall sublist alter inv f l i n k sublist lookup i n l Some k Forall P sublist alter f i n l Forall P f k Proof unfold sublist alter sublist lookup intros simplify option equality rewrite Forall app tauto Qed Lemma Forall reshape l szs Forall P l Forall Forall P reshape szs l Proof revert l induction szs simpl auto using Forall take Forall drop Qed Lemma Forall rev ind Q list A Prop Q x l P x Forall P l Q l Q l x l Forall P l Q l Proof intros l induction l using rev ind auto rewrite Forall app Forall singleton intros auto Qed Lemma Exists exists l Exists P l x x l P x Proof split induction 1 as x y x exists x by repeat constructor intros x Hin induction l by destruct not elem of nil x inversion Hin subst by left right auto Qed Lemma Exists inv x l Exists P x l P x Exists P l Proof inversion 1 intuition trivial

    Original URL path: http://robbertkrebbers.nl/research/ch2o/list.html (2015-08-10)
    Open archived version from archive

  • Module streams
    end Definition stail A s stream A stream A match s with s s end CoInductive stream equiv A s1 s2 stream A Prop scons equiv shead s1 shead s2 stream equiv stail s1 stail s2 stream equiv s1 s2 Instance stream equiv A Equiv stream A stream equiv Reserved Infix at level 20 Fixpoint slookup A i nat s stream A A match i with O shead s S i stail s i end where s i slookup i s Global Instance stream fmap FMap stream λ A B f cofix go s f shead s go stail s Fixpoint stake A n nat s stream A match n with 0 S n shead s stake n stail s end CoFixpoint srepeat A x A stream A x srepeat x Section stream properties Context A Type Implicit Types x y A Implicit Types s t stream A Lemma scons equiv s1 s2 shead s1 shead s2 stail s1 stail s2 s1 s2 Proof by constructor Qed Global Instance equal equivalence Equivalence equiv stream A Proof split now cofix intros constructor now cofix intros constructor cofix intros constructor etransitivity eauto Qed Global Instance scons proper x Proper scons x Proof

    Original URL path: http://robbertkrebbers.nl/research/ch2o/streams.html (2015-08-10)
    Open archived version from archive

  • Module vector
    n v w vec A n i v i w i v w Proof vec double ind v w done intros n v w IH x y Hi f equal apply Hi 0 fin apply IH intros i apply Hi FS i Qed Instance vec dec A dec x y A Decision x y n v w vec A n Decision v w Proof refine vec rect2 λ n v w vec A n v w v w left λ H x y cast if and dec x y H f equal eauto using vcons inj 1 vcons inj 2 Defined Similar to fin we provide an inversion principle that keeps the length fixed We define a tactic inv vec v to perform case analysis on v using this inversion principle Notation vec 0 inv Vector case0 Definition vec S inv A n P vec A S n Type Hcons x v P x v v P v Proof revert P Hcons refine match v with tt x v λ P Hcons Hcons x v end Defined Ltac inv vec v match type of v with vec 0 revert dependent v match goal with v P v apply vec 0 inv P end vec S n revert dependent v match goal with v P v apply vec S inv P end end The following tactic performs case analysis on all hypotheses of the shape fin 0 fin S n vec A 0 and vec A S n until no further case analyses are possible Ltac inv all vec fin block goal repeat match goal with v vec inv vec v intros i fin inv fin i intros end unblock goal We define a coercion from vec to list and show that it preserves the operations on vectors We also define a function to go in the other way but do not define it as a coercion as it would otherwise introduce ambiguity Fixpoint vec to list A n v vec A n list A match v with x v x vec to list v end Coercion vec to list vec list Notation list to vec Vector of list Lemma vec to list cons A n x v vec A n vec to list x v x vec to list v Proof done Qed Lemma vec to list app A n m v vec A n w vec A m vec to list v w vec to list v vec to list w Proof by induction v f equal Qed Lemma vec to list of list A l list A vec to list list to vec l l Proof by induction l f equal Qed Lemma vec to list length A n v vec A n length vec to list v n Proof induction v simpl by f equal Qed Lemma vec to list same length A B n v vec A n w vec B n length v length w Proof by rewrite vec to list length Qed Lemma vec

    Original URL path: http://robbertkrebbers.nl/research/ch2o/vector.html (2015-08-10)
    Open archived version from archive

  • Module numbers
    scope Infix div N div at level 35 N scope Infix mod N modulo at level 35 N scope Arguments N add simpl never Instance Injective Npos Proof by injection 1 Qed Instance N eq dec x y N Decision x y N eq dec Program Instance N le dec x y N Decision x y N match Ncompare x y with Gt right left end Next Obligation congruence Qed Program Instance N lt dec x y N Decision x y N match Ncompare x y with Lt left right end Next Obligation congruence Qed Instance N inhabited Inhabited N populate 1 N Instance PartialOrder N Proof repeat split red apply N le refl apply N le trans apply N le antisymm Qed Hint Extern 0 N reflexivity Notations and properties of Z Open Scope Z scope Infix Z le Z scope Notation x y z x y y z Z scope Notation x y z x y y z Z scope Notation x y z x y y z Z scope Notation x y z x y y z Z scope Notation x y z z x y y z z z Z scope Notation Z le only parsing Z scope Notation Z lt only parsing Z scope Infix div Z div at level 35 Z scope Infix mod Z modulo at level 35 Z scope Infix quot Z quot at level 35 Z scope Infix rem Z rem at level 35 Z scope Infix Z shiftl at level 35 Z scope Infix Z shiftr at level 35 Z scope Instance Injective Zpos Proof by injection 1 Qed Instance Injective Zneg Proof by injection 1 Qed Instance Z eq dec x y Z Decision x y Z eq dec Instance Z le dec x y Z Decision x y Z le dec Instance Z lt dec x y Z Decision x y Z lt dec Instance Z inhabited Inhabited Z populate 1 Instance PartialOrder Proof repeat split red apply Z le refl apply Z le trans apply Z le antisymm Qed Lemma Z pow pred r n m 0 m n n Z pred m n m Proof intros rewrite Z pow succ r Z succ pred done by apply Z lt le pred Qed Lemma Z quot range nonneg k x y 0 x k 0 y 0 x quot y k Proof intros destruct decide y 1 subst rewrite Z quot 1 r auto destruct decide x 0 subst rewrite Z quot 0 l auto with lia split apply Z quot pos lia transitivity x auto apply Z quot lt lia Qed Arguments Z to nat simpl never Arguments Z mul simpl never Arguments Z add simpl never Arguments Z opp simpl never Arguments Z pow simpl never Arguments Z div simpl never Arguments Z modulo simpl never Arguments Z quot simpl never Arguments Z rem simpl never Lemma Z to nat neq 0 pos x Z to nat x 0 nat 0 x Proof by destruct x Qed Lemma Z to nat neq 0 nonneg x Z to nat x 0 nat 0 x Proof by destruct x Qed Lemma Z mod pos x y 0 y 0 x mod y Proof apply Z mod pos bound Qed Hint Resolve Z lt le incl zpos Hint Resolve Z add nonneg pos Z add pos nonneg Z add nonneg nonneg zpos Hint Resolve Z mul nonneg nonneg Z mul pos pos zpos Hint Resolve Z pow pos nonneg Z pow nonneg zpos Hint Resolve Z mod pos Z div pos zpos Hint Extern 1000 lia zpos Lemma Z to nat nonpos x x 0 Z to nat x 0 nat Proof destruct x simpl auto using Z2Nat inj neg by intros Qed Lemma Z2Nat inj pow x y nat Z of nat x y x y Proof induction y as y IH by rewrite Z pow 0 r Nat pow 0 r by rewrite Nat pow succ r Nat2Z inj succ Z pow succ r Nat2Z inj mul IH by auto with zpos Qed Lemma Nat2Z divide n m Z of nat n Z of nat m n m nat Proof split rewrite Nat2Z id m at 2 intros i exists Z to nat i destruct decide 0 i Z by rewrite Z2Nat inj mul Nat2Z id by lia by rewrite Z to nat nonpos by auto using Z mul nonpos nonneg with lia intros i exists Z of nat i by rewrite Nat2Z inj mul Qed Lemma Z2Nat divide n m 0 n 0 m Z to nat n Z to nat m nat n m Proof intros by rewrite Nat2Z divide Z2Nat id by done Qed Lemma Z2Nat inj div x y Z of nat x div y x div y Proof destruct decide y 0 nat by subst destruct x apply Z div unique with x mod y nat left rewrite Nat2Z inj le 0 Nat2Z inj lt apply Nat mod bound pos lia by rewrite Nat2Z inj mul Nat2Z inj add Nat div mod Qed Lemma Z2Nat inj mod x y Z of nat x mod y x mod y Proof destruct decide y 0 nat by subst destruct x apply Z mod unique with x div y nat left rewrite Nat2Z inj le 0 Nat2Z inj lt apply Nat mod bound pos lia by rewrite Nat2Z inj mul Nat2Z inj add Nat div mod Qed Close Scope Z scope Notations and properties of Qc Open Scope Qc scope Delimit Scope Qc scope with Qc Notation 1 Q2Qc 1 Qc scope Notation 2 1 1 Qc scope Notation 1 Qcopp 1 Qc scope Notation 2 Qcopp 2 Qc scope Notation x y x y Qc scope Notation x y x y Qc scope Infix Qcle Qc scope Notation x y z x y y z Qc scope Notation x y z x y y z Qc scope Notation x y z x y y z Qc scope Notation x y z x y

    Original URL path: http://robbertkrebbers.nl/research/ch2o/numbers.html (2015-08-10)
    Open archived version from archive

  • Module ars
    Pstep y z rtc R x y R y z P y P z z rtc R x z P z Proof intros z p revert x z p Prefl Pstep refine rtc ind r weak eauto Qed Lemma rtc inv r x z rtc R x z x z y rtc R x y R y z Proof revert z apply rtc ind r eauto Qed Lemma nsteps once x y R x y nsteps R 1 x y Proof eauto Qed Lemma nsteps trans n m x y z nsteps R n x y nsteps R m y z nsteps R n m x z Proof induction 1 simpl eauto Qed Lemma nsteps r n x y z nsteps R n x y R y z nsteps R S n x z Proof induction 1 eauto Qed Lemma nsteps rtc n x y nsteps R n x y rtc R x y Proof induction 1 eauto Qed Lemma rtc nsteps x y rtc R x y n nsteps R n x y Proof induction 1 firstorder eauto Qed Lemma bsteps once n x y R x y bsteps R S n x y Proof eauto Qed Lemma bsteps plus r n m x y bsteps R n x y bsteps R n m x y Proof induction 1 simpl eauto Qed Lemma bsteps weaken n m x y n m bsteps R n x y bsteps R m x y Proof intros rewrite Minus le plus minus n m auto using bsteps plus r Qed Lemma bsteps plus l n m x y bsteps R n x y bsteps R m n x y Proof apply bsteps weaken auto with arith Qed Lemma bsteps S n x y bsteps R n x y bsteps R S n x y Proof apply bsteps weaken lia Qed Lemma bsteps trans n m x y z bsteps R n x y bsteps R m y z bsteps R n m x z Proof induction 1 simpl eauto using bsteps plus l Qed Lemma bsteps r n x y z bsteps R n x y R y z bsteps R S n x z Proof induction 1 eauto Qed Lemma bsteps rtc n x y bsteps R n x y rtc R x y Proof induction 1 eauto Qed Lemma rtc bsteps x y rtc R x y n bsteps R n x y Proof induction 1 exists 0 constructor naive solver eauto Qed Lemma bsteps ind r P nat A Prop x A Prefl n P n x Pstep n y z bsteps R n x y R y z P n y P S n z n z bsteps R n x z P n z Proof cut m y z bsteps R m y z n bsteps R n x y m n m m n m P m y P n m z intros help change n with 0 n eauto induction 1 as m x y z

    Original URL path: http://robbertkrebbers.nl/research/ch2o/ars.html (2015-08-10)
    Open archived version from archive