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 collections
    elem of join in H context guard setoid rewrite elem of guard in H context of option setoid rewrite elem of of option in H context of list setoid rewrite elem of of list in H end repeat match goal with context setoid rewrite elem of subseteq context setoid rewrite subset spec context setoid rewrite elem of equiv empty context setoid rewrite elem of equiv alt context setoid rewrite elem of equiv empty L context setoid rewrite elem of equiv alt L context setoid rewrite elem of empty context setoid rewrite elem of singleton context setoid rewrite elem of union context setoid rewrite elem of intersection context setoid rewrite elem of difference context setoid rewrite elem of fmap context mret setoid rewrite elem of ret context setoid rewrite elem of bind context mjoin setoid rewrite elem of join context guard setoid rewrite elem of guard context of option setoid rewrite elem of of option context of list setoid rewrite elem of of list end The tactic solve elem of tac composes the above tactic with intuition For goals that do not involve map or quantifiers this tactic is generally powerful enough This tactic either fails or proves the goal Tactic Notation solve elem of tactic3 tac simpl in decompose empty unfold elem of solve intuition simplify equality tac Tactic Notation solve elem of solve elem of auto For goals with quantifiers we could use the above tactic but with firstorder instead of intuition as finishing tactic However firstorder fails or loops on very small goals generated by solve elem of already We use the naive solver tactic as a substitute This tactic either fails or proves the goal Tactic Notation esolve elem of tactic3 tac simpl in decompose empty unfold elem of naive solver tac Tactic Notation esolve elem of esolve elem of eauto More theorems Section collection Context Collection A C Global Instance Lattice C Proof split apply firstorder auto solve elem of Qed Lemma intersection singletons x x x x Proof esolve elem of Qed Lemma difference twice X Y X Y Y X Y Proof esolve elem of Qed Lemma subseteq empty difference X Y X Y X Y Proof esolve elem of Qed Lemma difference diag X X X Proof esolve elem of Qed Lemma difference union distr l X Y Z X Y Z X Z Y Z Proof esolve elem of Qed Lemma difference intersection distr l X Y Z X Y Z X Z Y Z Proof esolve elem of Qed Section leibniz Context LeibnizEquiv C Lemma intersection singletons L x x x x Proof unfold leibniz apply intersection singletons Qed Lemma difference twice L X Y X Y Y X Y Proof unfold leibniz apply difference twice Qed Lemma subseteq empty difference L X Y X Y X Y Proof unfold leibniz apply subseteq empty difference Qed Lemma difference diag L X X X Proof unfold leibniz apply difference diag Qed Lemma difference union distr l L X Y Z X Y Z X Z Y Z Proof unfold leibniz apply difference union distr l Qed Lemma difference intersection distr l L X Y Z X Y Z X Z Y Z Proof unfold leibniz apply difference intersection distr l Qed End leibniz Section dec Context X Y C Decision X Y Lemma not elem of intersection x X Y x X Y x X x Y Proof rewrite elem of intersection destruct decide x X tauto Qed Lemma not elem of difference x X Y x X Y x X x Y Proof rewrite elem of difference destruct decide x Y tauto Qed Lemma union difference X Y X Y Y X Y X Proof split intros x rewrite elem of union elem of difference intuition destruct decide x X intuition Qed Lemma non empty difference X Y X Y Y X Proof intros HXY1 HXY2 Hdiff destruct HXY2 intros x destruct decide x X esolve elem of Qed Lemma empty difference subseteq X Y X Y X Y Proof intros x apply dec stable esolve elem of Qed Context LeibnizEquiv C Lemma union difference L X Y X Y Y X Y X Proof unfold leibniz apply union difference Qed Lemma non empty difference L X Y X Y Y X Proof unfold leibniz apply non empty difference Qed Lemma empty difference subseteq L X Y X Y X Y Proof unfold leibniz apply empty difference subseteq Qed End dec End collection Section collection ops Context CollectionOps A C Lemma elem of intersection with list f A A option A Xs Y x x intersection with list f Y Xs xs y Forall2 xs Xs y Y foldr λ x f x Some y xs Some x Proof split revert x induction Xs simpl intros x HXs eexists x intuition rewrite elem of intersection with in HXs destruct HXs as x1 x2 destruct IHXs x2 as xs y hy trivial eexists x1 xs y intuition simplify option equality auto intros xs y Hxs Hx revert x Hx induction Hxs intros simplify option equality done rewrite elem of intersection with naive solver Qed Lemma intersection with list ind P Q A Prop f Xs Y y y Y P y Forall λ X x x X Q x Xs x y z Q x P y f x y Some z P z x x intersection with list f Y Xs P x Proof intros HY HXs Hf induction Xs simplify option equality done intros x Hx rewrite elem of intersection with in Hx decompose Forall destruct Hx as eauto Qed End collection ops Sets without duplicates up to an equivalence Section NoDup Context SimpleCollection A B R relation A Equivalence R Definition elem of upto x A X B y y X R x y Definition set NoDup X B x y x X y X R x y x y Global Instance Proper iff elem of upto x Proof intros E unfold elem of upto by setoid rewrite E

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


  • Module fin_collections
    Proof destruct elements X as x l eqn HX right left apply equiv empty intros x by rewrite elem of elements HX elem of nil exists x rewrite elem of elements HX by left Qed Lemma collection choose X X x x X Proof intros by destruct collection choose or empty X Qed Lemma collection choose L LeibnizEquiv C X X x x X Proof unfold leibniz apply collection choose Qed Lemma size pos elem of X 0 size X x x X Proof intros Hsz destruct collection choose or empty X as HX done contradict Hsz rewrite HX size empty lia Qed Lemma size 1 elem of X size X 1 x X x Proof intros E destruct size pos elem of X auto with lia exists x apply elem of equiv split rewrite elem of singleton eauto using size singleton inv solve elem of Qed Lemma size union X Y X Y size X Y size X size Y Proof intros E unfold size collection size simpl rewrite app length apply Permutation length NoDup Permutation apply NoDup elements apply NoDup app repeat split try apply NoDup elements intros x rewrite elem of elements esolve elem of intros rewrite elem of app elem of elements solve elem of Qed Instance elem of dec slow x A X C Decision x X 100 Proof refine cast if decide rel x elements X by rewrite elem of elements Defined Global Program Instance collection subseteq dec slow X Y C Decision X Y 100 match decide rel size X Y 0 with left E1 left right E1 right end Next Obligation intros x Ex apply dec stable intro destruct proj1 elem of empty x apply size empty inv E1 by rewrite elem of difference Qed Next Obligation intros E2 destruct E1 apply size empty iff equiv empty intros x rewrite elem of difference intros E3 by apply E2 in E3 Qed Lemma size union alt X Y size X Y size X size Y X Proof rewrite size union by solve elem of setoid replace Y X with Y X X by esolve elem of rewrite union difference commutative solve elem of Qed Lemma subseteq size X Y X Y size X size Y Proof intros rewrite union difference X Y size union alt by done lia Qed Lemma subset size X Y X Y size X size Y Proof intros rewrite union difference X Y by solve elem of rewrite size union alt difference twice cut size Y X 0 lia by apply size non empty iff non empty difference Qed Lemma collection wf wf strict subseteq C Proof apply wf projected size auto using subset size lt wf Qed Lemma collection ind P C Prop Proper iff P P x X x X P X P x X X P X Proof intros Hemp Hadd apply well founded induction with apply collection wf intros X IH destruct collection choose or empty X as x HX rewrite union difference x X

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

  • Module listset
    listset car X Proof destruct X as l split by intros simplify equality intros Hl destruct l as x l done feed inversion Hl x left Qed Global Instance listset empty dec X listset A Decision X Proof refine cast if decide listset car X abstract by rewrite listset empty alt Defined Context x y A Decision x y Instance listset intersection Intersection listset A λ l k let l l in let k k in Listset list intersection l k Instance listset difference Difference listset A λ l k let l l in let k k in Listset list difference l k Instance listset intersection with IntersectionWith A listset A λ f l k let l l in let k k in Listset list intersection with f l k Instance listset filter Filter A listset A λ P l let l l in Listset filter P l Instance Collection A listset A Proof split apply intros apply elem of list intersection intros apply elem of list difference Qed Instance listset elems Elements A listset A remove dups listset car Global Instance FinCollection A listset A Proof split apply intros apply elem of remove dups intros apply NoDup remove dups Qed Global Instance CollectionOps A listset A Proof split apply intros apply elem of list intersection with intros apply elem of list filter Qed End listset These instances are declared using Hint Extern to avoid too eager type class search Hint Extern 1 ElemOf listset eapply listset elem of typeclass instances Hint Extern 1 Empty listset eapply listset empty typeclass instances Hint Extern 1 Singleton listset eapply listset singleton typeclass instances Hint Extern 1 Union listset eapply listset union typeclass instances Hint Extern 1 Intersection listset eapply listset intersection typeclass instances Hint Extern 1 IntersectionWith listset eapply listset intersection with

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

  • Module fresh_numbers
    apply collection fold proper solve proper intros rewrite N max assoc f equal apply N max comm Qed Lemma Nmax max FinCollection N C X x x X x Nmax X N Proof apply collection fold ind λ b X x X x b N solve proper solve elem of solve elem of eauto using N le max l N le max r N le trans Qed Instance Nfresh FinCollection

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

  • Module prelude
    Module prelude Require Export base tactics decidable orders option vector numbers ars collections fin collections listset list lexico Generated by coq2html

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

  • Module fin_maps
    decide i j as rewrite lookup insert lookup insert ne intuition congruence intros apply lookup insert by rewrite lookup insert ne Qed Lemma lookup insert None A m M A i j x i x m j None m j None i j Proof split by intros rewrite lookup insert ne destruct decide i j as rewrite lookup insert lookup insert ne intuition congruence Qed Lemma insert id A m M A i x m i Some x i x m m Proof intros apply map eq intros j destruct decide i j as by rewrite lookup insert lookup insert ne by done Qed Lemma insert included A R Reflexive R m M A i x y m i Some y R y x map included R m i x m Proof intros j destruct decide i j as rewrite lookup insert destruct m j eauto rewrite lookup insert ne by done by destruct m j Qed Lemma insert subseteq A m M A i x m i None m i x m Proof apply partial alter subseteq Qed Lemma insert subset A m M A i x m i None m i x m Proof intro apply partial alter subset eauto Qed Lemma insert subseteq r A m1 m2 M A i x m1 i None m1 m2 m1 i x m2 Proof rewrite map subseteq spec intros j destruct decide j i as congruence rewrite lookup insert ne auto Qed Lemma insert delete subseteq A m1 m2 M A i x m1 i None i x m1 m2 m1 delete i m2 Proof rewrite map subseteq spec intros Hi Hix j y Hj destruct decide i j as congruence rewrite lookup delete ne by done apply Hix by rewrite lookup insert ne by done Qed Lemma delete insert subseteq A m1 m2 M A i x m1 i Some x delete i m1 m2 m1 i x m2 Proof rewrite map subseteq spec intros Hix Hi j y Hj destruct decide i j as rewrite lookup insert congruence rewrite lookup insert ne by done apply Hi by rewrite lookup delete ne Qed Lemma insert delete subset A m1 m2 M A i x m1 i None i x m1 m2 m1 delete i m2 Proof intros Hm12 Hm21 split eauto using insert delete subseteq contradict Hm21 apply delete insert subseteq auto eapply lookup weaken Hm12 by rewrite lookup insert Qed Lemma insert subset inv A m1 m2 M A i x m1 i None i x m1 m2 m2 m2 i x m2 m1 m2 m2 i None Proof intros Hi Hm1m2 exists delete i m2 split ands rewrite insert delete done eapply lookup weaken strict include eauto by rewrite lookup insert eauto using insert delete subset by rewrite lookup delete Qed Lemma fmap insert A B f A B m M A i x f i x m i f x f m Proof apply map eq intros i destruct decide i i as by rewrite lookup fmap lookup insert by rewrite lookup fmap lookup insert ne lookup fmap by done Qed Lemma insert empty A i x A i x i x Proof done Qed Properties of the singleton maps Lemma lookup singleton Some A i j x y A i x j Some y i j x y Proof unfold singleton map singleton rewrite lookup insert Some lookup empty simpl intuition congruence Qed Lemma lookup singleton None A i j x A i x j None i j Proof unfold singleton map singleton rewrite lookup insert None lookup empty simpl tauto Qed Lemma lookup singleton A i x A i x i Some x Proof by rewrite lookup singleton Some Qed Lemma lookup singleton ne A i j x A i j i x j None Proof by rewrite lookup singleton None Qed Lemma map non empty singleton A i x A i x Proof intros Hix apply f equal i in Hix by rewrite lookup empty lookup singleton in Hix Qed Lemma insert singleton A i x y A i y i x i y Proof unfold singleton map singleton insert map insert by rewrite partial alter compose Qed Lemma alter singleton A f A A i x alter f i i x i f x Proof intros apply map eq intros i destruct decide i i as by rewrite lookup alter lookup singleton by rewrite lookup alter ne lookup singleton ne Qed Lemma alter singleton ne A f A A i j x i j alter f i j x j x Proof intros apply map eq intros i by destruct decide i i as rewrite lookup alter lookup singleton ne lookup alter ne by done Qed Properties of the map operations Lemma fmap empty A B f A B f Proof apply map empty intros i by rewrite lookup fmap lookup empty Qed Lemma omap empty A B f A option B omap f Proof apply map empty intros i by rewrite lookup omap lookup empty Qed Lemma omap singleton A B f A option B i x y f x Some y omap f i x i y Proof intros apply map eq intros j destruct decide i j as by rewrite lookup omap lookup singleton by rewrite lookup omap lookup singleton ne Qed Properties of conversion to lists Lemma map to list unique A m M A i x y i x map to list m i y map to list m x y Proof rewrite elem of map to list congruence Qed Lemma NoDup fst map to list A m M A NoDup map to list m 1 Proof eauto using NoDup fmap fst map to list unique NoDup map to list Qed Lemma elem of map of list 1 help A l list K A i x i x l y i y l y x map of list l i Some x Proof induction l as j y l IH csimpl by rewrite elem of nil setoid rewrite elem of cons intros Hdup simplify equality by rewrite lookup insert destruct decide i j as rewrite lookup insert f equal eauto rewrite lookup insert ne by done eauto Qed Lemma elem of map of list 1 A l list K A i x NoDup l 1 i x l map of list l i Some x Proof intros Hx apply elem of map of list 1 help eauto using NoDup fmap fst intros y revert Hx rewrite elem of list lookup intros i Hi j Hj cut i j naive solver apply NoDup lookup with l 1 i by rewrite list lookup fmap Hi Hj Qed Lemma elem of map of list 2 A l list K A i x map of list l i Some x i x l Proof induction l as j y l IH simpl by rewrite lookup empty rewrite elem of cons destruct decide i j as rewrite lookup insert lookup insert ne intuition congruence Qed Lemma elem of map of list A l list K A i x NoDup l 1 i x l map of list l i Some x Proof split auto using elem of map of list 1 elem of map of list 2 Qed Lemma not elem of map of list 1 A l list K A i i l 1 map of list l i None Proof rewrite elem of list fmap eq None not Some intros Hi x destruct Hi exists i x simpl auto using elem of map of list 2 Qed Lemma not elem of map of list 2 A l list K A i map of list l i None i l 1 Proof induction l as j y l IH csimpl rewrite elem of nil tauto rewrite elem of cons destruct decide i j simplify equality by rewrite lookup insert by rewrite lookup insert ne intuition Qed Lemma not elem of map of list A l list K A i i l 1 map of list l i None Proof red auto using not elem of map of list 1 not elem of map of list 2 Qed Lemma map of list proper A l1 l2 list K A NoDup l1 1 l1 ₚ l2 map of list l1 map of list l2 Proof intros Hperm apply map eq intros i apply option eq intros x by rewrite elem of map of list rewrite Hperm Qed Lemma map of list inj A l1 l2 list K A NoDup l1 1 NoDup l2 1 map of list l1 map of list l2 l1 ₚ l2 Proof intros Hl1l2 apply NoDup Permutation auto using NoDup fmap 1 fst intros i x by rewrite elem of map of list Hl1l2 Qed Lemma map of to list A m M A map of list map to list m m Proof apply map eq intros i apply option eq intros x by rewrite elem of map of list elem of map to list by auto using NoDup fst map to list Qed Lemma map to of list A l list K A NoDup l 1 map to list map of list l ₚ l Proof auto using map of list inj NoDup fst map to list map of to list Qed Lemma map to list inj A m1 m2 M A map to list m1 ₚ map to list m2 m1 m2 Proof intros rewrite map of to list m1 map of to list m2 auto using map of list proper NoDup fst map to list Qed Lemma map to of list flip A m1 M A l2 map to list m1 ₚ l2 m1 map of list l2 Proof intros rewrite map of to list m1 auto using map of list proper NoDup fst map to list Qed Lemma map to list empty A map to list nil K A Proof apply elem of nil inv intros i x rewrite elem of map to list apply lookup empty Some Qed Lemma map to list insert A m M A i x m i None map to list i x m ₚ i x map to list m Proof intros apply map of list inj csimpl apply NoDup fst map to list constructor auto using NoDup fst map to list rewrite elem of list fmap intros Hlookup subst simpl in rewrite elem of map to list in Hlookup congruence by rewrite map of to list Qed Lemma map of list nil A map of list nil K A Proof done Qed Lemma map of list cons A l list K A i x map of list i x l i x map of list l Proof done Qed Lemma map to list empty inv alt A m M A map to list m ₚ m Proof rewrite map to list empty apply map to list inj Qed Lemma map to list empty inv A m M A map to list m m Proof intros Hm apply map to list empty inv alt by rewrite Hm Qed Lemma map to list insert inv A m M A l i x map to list m ₚ i x l m i x map of list l Proof intros Hperm apply map to list inj assert i l 1 NoDup l 1 as rewrite NoDup cons change NoDup i x l 1 rewrite Hperm auto using NoDup fst map to list rewrite Hperm map to list insert map to of list auto using not elem of map of list 1 Qed Lemma map choose A m M A m i x m i Some x Proof intros Hemp destruct map to list m as i x l eqn Hm destruct Hemp eauto using map to list empty inv exists i x rewrite elem of map to list Hm by left Qed Properties of conversion from collections Lemma lookup map of collection A FinCollection K C f K option A X i x map of collection f X i Some x i X f i Some x Proof assert NoDup fst omap λ i i f i elements X induction NoDup elements X as i l csimpl constructor destruct f i as x csimpl auto constructor auto rewrite elem of list fmap setoid rewrite elem of list omap by intros simplify option equality unfold map of collection rewrite elem of map of list by done rewrite elem of list omap setoid rewrite elem of elements split intros simplify option equality eauto intros exists i simplify option equality eauto Qed Induction principles Lemma map ind A P M A Prop P i x m m i None P m P i x m m P m Proof intros Hins cut l NoDup l 1 m map to list m ₚ l P m intros help m apply help map to list m auto using NoDup fst map to list induction l as i x l IH intros Hnodup m Hml apply map to list empty inv alt in Hml by subst inversion clear Hnodup apply map to list insert inv in Hml subst m apply Hins by apply not elem of map of list 1 apply IH auto using map to of list Qed Lemma map to list length A m1 m2 M A m1 m2 length map to list m1 length map to list m2 Proof revert m2 induction m1 as i x m IH using map ind intros m2 Hm2 rewrite map to list empty simpl apply neq 0 lt intros Hlen symmetry in Hlen apply nil length inv map to list empty inv in Hlen rewrite Hlen in Hm2 destruct irreflexivity Hm2 intros m2 Hm2 destruct insert subset inv m m2 i x as m2 auto subst rewrite map to list insert simpl auto with arith Qed Lemma map wf A wf strict subseteq M A Proof apply wf projected length map to list by apply map to list length by apply lt wf Qed Properties of the map Forall predicate Section map Forall Context A P K A Prop Lemma map Forall to list m map Forall P m Forall curry P map to list m Proof rewrite Forall forall split intros Hforall i x rewrite elem of map to list by apply Hforall i x intros Hforall i x rewrite elem of map to list by apply Hforall i x Qed Lemma map Forall empty map Forall P Proof intros i x by rewrite lookup empty Qed Lemma map Forall impl Q K A Prop m map Forall P m i x P i x Q i x map Forall Q m Proof unfold map Forall naive solver Qed Lemma map Forall insert 11 m i x map Forall P i x m P i x Proof intros Hm by apply Hm rewrite lookup insert Qed Lemma map Forall insert 12 m i x m i None map Forall P i x m map Forall P m Proof intros Hm j y apply Hm by rewrite lookup insert ne by congruence Qed Lemma map Forall insert 2 m i x P i x map Forall P m map Forall P i x m Proof intros j y rewrite lookup insert Some naive solver Qed Lemma map Forall insert m i x m i None map Forall P i x m P i x map Forall P m Proof naive solver eauto using map Forall insert 11 map Forall insert 12 map Forall insert 2 Qed Lemma map Forall ind Q M A Prop Q m i x m i None P i x map Forall P m Q m Q i x m m map Forall P m Q m Proof intros Hnil Hinsert m induction m using map ind auto rewrite map Forall insert by done intros eauto Qed Context i x Decision P i x Global Instance map Forall dec m Decision map Forall P m Proof refine cast if decide Forall curry P map to list m by rewrite map Forall to list Defined Lemma map not Forall m M A map Forall P m i x m i Some x P i x Proof split intros i x Hm specialize Hm i x tauto rewrite map Forall to list intros Hm apply not Forall Exists Exists exists in Hm destruct Hm as i x exists i x by rewrite elem of map to list Qed End map Forall Properties of the merge operation Section merge Context A f option A option A option A Context PropHolds f None None None Global Instance LeftId None f LeftId merge f Proof intros apply map eq intros by rewrite lookup merge f lookup empty left id L None f Qed Global Instance RightId None f RightId merge f Proof intros apply map eq intros by rewrite lookup merge f lookup empty right id L None f Qed Lemma merge commutative m1 m2 i f m1 i m2 i f m2 i m1 i merge f m1 m2 merge f m2 m1 Proof intros apply map eq intros by rewrite lookup merge f Qed Global Instance Commutative f Commutative merge f Proof intros apply merge commutative intros by apply commutative f Qed Lemma merge associative m1 m2 m3 i f m1 i f m2 i m3 i f f m1 i m2 i m3 i merge f m1 merge f m2 m3 merge f merge f m1 m2 m3 Proof intros apply map eq intros by rewrite lookup merge f Qed Global Instance Associative f Associative merge f Proof intros apply merge associative intros by apply associative L f Qed Lemma merge idempotent m1 i f m1 i m1 i m1 i merge f m1 m1 m1 Proof intros apply map eq intros by rewrite lookup merge f Qed Global Instance Idempotent f Idempotent merge f Proof intros apply merge idempotent intros by apply idempotent f Qed End merge Section more merge Context A B C f option A option B option C Context PropHolds f None None None Lemma merge Some m1 m2 m i m i f m1 i m2 i merge f m1 m2 m Proof split intros apply lookup merge intros Hlookup apply map eq intros rewrite Hlookup apply lookup merge Qed Lemma merge empty merge f Proof apply map eq intros by rewrite lookup merge f lookup empty Qed Lemma partial alter merge g g1 g2 m1 m2 i g f m1 i m2 i f g1 m1 i g2 m2 i partial alter g i merge f m1 m2 merge f partial alter g1 i m1 partial alter g2 i m2 Proof intro apply map eq intros j destruct decide i j subst by rewrite lookup merge lookup partial alter lookup merge by rewrite lookup merge lookup partial alter ne lookup merge Qed Lemma partial alter merge l g g1 m1 m2 i g f m1 i m2 i f g1 m1 i m2 i partial alter g i merge f m1 m2 merge f partial alter g1 i m1 m2 Proof intro apply map eq intros j destruct decide i j subst by rewrite lookup merge lookup partial alter lookup merge by rewrite lookup merge lookup partial alter ne lookup merge Qed Lemma partial alter merge r g g2 m1 m2 i g f m1 i m2 i f m1 i g2 m2 i partial alter g i merge f m1 m2 merge f m1 partial alter g2 i m2 Proof intro apply map eq intros j destruct decide i j subst by rewrite lookup merge lookup partial alter lookup merge by rewrite lookup merge lookup partial alter ne lookup merge Qed Lemma insert merge m1 m2 i x y z f Some y Some z Some x i x merge f m1 m2 merge f i y m1 i z m2 Proof by intros apply partial alter merge Qed Lemma merge singleton i x y z f Some y Some z Some x merge f i y i z i x Proof intros unfold singleton map singleton simpl by erewrite insert merge merge empty by eauto Qed Lemma insert merge l m1 m2 i x y f Some y m2 i Some x i x merge f m1 m2 merge f i y m1 m2 Proof by intros apply partial alter merge l Qed Lemma insert merge r m1 m2 i x z f m1 i Some z Some x i x merge f m1 m2 merge f m1 i z m2 Proof by intros apply partial alter merge r Qed End more merge Properties on the map Forall2 relation Section Forall2 Context A B R A B Prop P A Prop Q B Prop Context x y Decision R x y x Decision P x y Decision Q y Let f mx option A my option B option bool match mx my with Some x Some y Some bool decide R x y Some x None Some bool decide P x None Some y Some bool decide Q y None None None end Lemma map Forall2 alt m1 M A m2 M B map Forall2 R P Q m1 m2 map Forall λ Is true merge f m1 m2 Proof split intros Hm i P rewrite lookup merge by done intros specialize Hm i destruct m1 i m2 i simplify equality auto using bool decide pack intros Hm i specialize Hm i rewrite lookup merge in Hm by done destruct m1 i m2 i simplify equality auto by eapply bool decide unpack Hm Qed Global Instance map Forall2 dec x y Decision R x y x Decision P x y Decision Q y m1 m2 Decision map Forall2 R P Q m1 m2 Proof refine cast if decide map Forall λ Is true merge f m1 m2 abstract by rewrite map Forall2 alt Defined Due to the finiteness of finite maps we can extract a witness if the relation does not hold Lemma map not Forall2 m1 M A m2 M B map Forall2 R P Q m1 m2 i x y m1 i Some x m2 i Some y R x y x m1 i Some x m2 i None P x y m1 i None m2 i Some y Q y Proof split rewrite map Forall2 alt map not Forall intros i Hm exists i rewrite lookup merge in Hm by done destruct m1 i m2 i naive solver auto 2 using bool decide pack by intros i x y x y Hm specialize Hm i simplify option equality Qed End Forall2 Properties on the disjoint maps Lemma map disjoint spec A m1 m2 M A m1 m2 i x y m1 i Some x m2 i Some y False Proof split intros Hm i specialize Hm i destruct m1 i m2 i naive solver Qed Lemma map disjoint alt A m1 m2 M A m1 m2 i m1 i None m2 i None Proof split intros Hm1m2 i specialize Hm1m2 i destruct m1 i m2 i naive solver Qed Lemma map not disjoint A m1 m2 M A m1 m2 i x1 x2 m1 i Some x1 m2 i Some x2 Proof unfold disjoint map disjoint rewrite map not Forall2 by solve decision split naive solver intros i x y x y naive solver Qed Global Instance Symmetric disjoint M A Proof intros A m1 m2 rewrite map disjoint spec naive solver Qed Lemma map disjoint empty l A m M A m Proof rewrite map disjoint spec intros i x y by rewrite lookup empty Qed Lemma map disjoint empty r A m M A m Proof rewrite map disjoint spec intros i x y by rewrite lookup empty Qed Lemma map disjoint weaken A m1 m1 m2 m2 M A m1 m2 m1 m1 m2 m2 m1 m2 Proof rewrite map subseteq spec map disjoint spec eauto Qed Lemma map disjoint weaken l A m1 m1 m2 M A m1 m2 m1 m1 m1 m2 Proof eauto using map disjoint weaken Qed Lemma map disjoint weaken r A m1 m2 m2 M A m1 m2 m2 m2 m1 m2 Proof eauto using map disjoint weaken Qed Lemma map disjoint Some l A m1 m2 M A i x m1 m2 m1 i Some x m2 i None Proof rewrite map disjoint spec eq None not Some intros eauto Qed Lemma map disjoint Some r A m1 m2 M A i x m1 m2 m2 i Some x m1 i None Proof rewrite symmetry iff apply map disjoint Some l Qed Lemma map disjoint singleton l A m M A i x i x m m i None Proof split rewrite map disjoint spec intro apply map disjoint Some l i x x auto using lookup singleton intros j y1 y2 destruct decide i j as rewrite lookup singleton intuition congruence by rewrite lookup singleton ne Qed Lemma map disjoint singleton r A m M A i x m i x m i None Proof by rewrite symmetry iff map disjoint singleton l Qed Lemma map disjoint singleton l 2 A m M A i x m i None i x m Proof by rewrite map disjoint singleton l Qed Lemma map disjoint singleton r 2 A m M A i x m i None m i x Proof by rewrite map disjoint singleton r Qed Lemma map disjoint delete l A m1 m2 M A i m1 m2 delete i m1 m2 Proof rewrite map disjoint alt intros Hdisjoint j destruct Hdisjoint j auto rewrite lookup delete None tauto Qed Lemma map disjoint delete r A m1 m2 M A i m1 m2 m1 delete i m2 Proof symmetry by apply map disjoint delete l Qed Properties of the union with operation Section union with Context A f A A option A Lemma lookup union with m1 m2 i union with f m1 m2 i union with f m1 i m2 i Proof by rewrite lookup merge Qed Lemma lookup union with Some m1 m2 i z union with f m1 m2 i Some z m1 i Some z m2 i None m1 i None m2 i Some z x y m1 i Some x m2 i Some y f x y Some z Proof rewrite lookup union with destruct m1 i m2 i compute naive solver Qed Global Instance LeftId eq M A union with f Proof unfold union with map union with apply Qed Global Instance RightId eq M A union with f Proof unfold union with map union with apply Qed Lemma union with commutative m1 m2 i x y m1 i Some x m2 i Some y f x y f y x union with f m1 m2 union with f m2 m1 Proof intros apply merge commutative intros i destruct m1 i eqn m2 i eqn simpl eauto Qed Global Instance Commutative f Commutative eq M A union with f Proof intros apply union with commutative eauto Qed Lemma union with idempotent m i x m i Some x f x x Some x union with f m m m Proof intros apply merge idempotent intros i destruct m i eqn simpl eauto Qed Lemma alter union with g A A m1 m2 i x y m1 i Some x m2 i Some y g f x y f g x g y alter g i union with f m1 m2 union with f alter g i m1 alter g i m2 Proof intros apply partial alter merge destruct m1 i eqn m2 i eqn simpl eauto Qed Lemma alter union with l g A A m1 m2 i x y m1 i Some x m2 i Some y g f x y f g x y y m1 i None m2 i Some y g y y alter g i union with f m1 m2 union with f alter g i m1 m2 Proof intros apply partial alter merge l destruct m1 i eqn m2 i eqn f equal auto Qed Lemma alter union with r g A A m1 m2 i x y m1 i Some x m2 i Some y g f x y f x g y x m1 i Some x m2 i None g x x alter g i union with f m1 m2 union with f m1 alter g i m2 Proof intros apply partial alter merge r destruct m1 i eqn m2 i eqn f equal auto Qed Lemma delete union with m1 m2 i delete i union with f m1 m2 union with f delete i m1 delete i m2 Proof by apply partial alter merge Qed Lemma foldr delete union with m1 m2 M A is foldr delete union with f m1 m2 is union with f foldr delete m1 is foldr delete m2 is Proof induction is simpl done by rewrite IHis delete union with Qed Lemma insert union with m1 m2 i x y z f x y Some z i z union with f m1 m2 union with f i x m1 i y m2 Proof by intros apply partial alter merge Qed Lemma insert union with l m1 m2 i x m2 i None i x union with f m1 m2 union with f i x m1 m2 Proof intros Hm2 unfold union with map union with by erewrite insert merge l by by rewrite Hm2 Qed Lemma insert union with r m1 m2 i x m1 i None i x union with f m1 m2 union with f m1 i x m2 Proof intros Hm1 unfold union with map union with by erewrite insert merge r by by rewrite Hm1 Qed End union with Properties of the union operation Global Instance LeftId eq M A Global Instance RightId eq M A Global Instance Associative eq M A Proof intros A m1 m2 m3 unfold union map union union with map union with apply merge associative intros i by destruct m1 i m2 i m3 i Qed Global Instance Idempotent eq M A Proof intros A by apply union with idempotent Qed Lemma lookup union Some raw A m1 m2 M A i x m1 m2 i Some x m1 i Some x m1 i None m2 i Some x Proof unfold union map union union with map union with rewrite lookup merge destruct m1 i m2 i compute intuition congruence Qed Lemma lookup union None A m1 m2 M A i m1 m2 i None m1 i None m2 i None Proof unfold union map union union with map union with rewrite lookup merge destruct m1 i m2 i compute intuition congruence Qed Lemma map positive l A m1 m2 M A m1 m2 m1 Proof intros Hm apply map empty intros i apply f equal i in Hm rewrite lookup empty lookup union None in Hm tauto Qed Lemma map positive l alt A m1 m2 M A m1 m1 m2 Proof eauto using map positive l Qed Lemma lookup union Some A m1 m2 M A i x m1 m2 m1 m2 i Some x m1 i Some x m2 i Some x Proof intros Hdisjoint rewrite lookup union Some raw intuition eauto using map disjoint Some r Qed Lemma lookup union Some l A m1 m2 M A i x m1 i Some x m1 m2 i Some x Proof intro rewrite lookup union Some raw intuition Qed Lemma lookup union Some r A m1 m2 M A i x m1 m2 m2 i Some x m1 m2 i Some x Proof intro rewrite lookup union Some intuition Qed Lemma map union commutative A m1 m2 M A m1 m2 m1 m2 m2 m1 Proof intros Hdisjoint apply merge commutative union with λ x Some x intros i specialize Hdisjoint i destruct m1 i m2 i compute naive solver Qed Lemma map subseteq union A m1 m2 M A m1 m2 m1 m2 m2 Proof rewrite map subseteq spec intros Hm1m2 apply map eq intros i apply option eq intros x rewrite lookup union Some raw split by intuition intros Hm2 specialize Hm1m2 i destruct m1 i as y by auto rewrite Hm1m2 y eq refl in Hm2 intuition congruence Qed Lemma map union subseteq l A m1 m2 M A m1 m1 m2 Proof rewrite map subseteq spec intros i x rewrite lookup union Some raw tauto Qed Lemma map union subseteq r A m1 m2 M A m1 m2 m2 m1 m2 Proof intros rewrite map union commutative by done by apply map union subseteq l Qed Lemma map union subseteq l alt A m1 m2 m3 M A m1 m2 m1 m2 m3 Proof intros transitivity m2 auto using map union subseteq l Qed Lemma map union subseteq r alt A m1 m2 m3 M A m2 m3 m1 m3 m1 m2 m3 Proof intros transitivity m3 auto using map union subseteq r Qed Lemma map union preserving l A m1 m2 m3 M A m1 m2 m3 m1 m3 m2 Proof rewrite map subseteq spec intros rewrite lookup union Some raw naive solver Qed Lemma map union preserving r A m1 m2 m3 M A m2 m3 m1 m2 m1 m3 m2 m3 Proof intros rewrite map union commutative m3 by eauto using map disjoint weaken l by apply map union preserving l Qed Lemma map union reflecting l A m1 m2 m3 M A m3 m1 m3 m2 m3 m1 m3 m2 m1 m2 Proof rewrite map subseteq spec intros Hm31 Hm32 Hm i x specialize Hm i x rewrite lookup union Some in Hm by done destruct Hm auto by rewrite map disjoint spec in Hm31 destruct Hm31 i x x Qed Lemma map union reflecting r A m1 m2 m3 M A m1 m3 m2 m3 m1 m3 m2 m3 m1 m2 Proof intros rewrite map union commutative m3 by done by apply map union reflecting l Qed Lemma map union cancel l A m1 m2 m3 M A m1 m3 m2 m3 m3 m1 m3 m2 m1 m2 Proof intros apply anti symmetric apply map union reflecting l with m3 auto using reflexive eq R Qed Lemma map union cancel r A m1 m2 m3 M A m1 m3 m2 m3 m1 m3 m2 m3 m1 m2 Proof intros apply anti symmetric apply map union reflecting r with m3 auto using reflexive eq R Qed Lemma map disjoint union l A m1 m2 m3 M A m1 m2 m3 m1 m3 m2 m3 Proof rewrite map disjoint alt setoid rewrite lookup union None naive solver Qed Lemma map disjoint union r A m1 m2 m3 M A m1 m2 m3 m1 m2 m1 m3 Proof rewrite map disjoint alt setoid rewrite lookup union None naive solver Qed Lemma map disjoint union l 2 A m1 m2 m3 M A m1 m3 m2 m3 m1 m2 m3 Proof by rewrite map disjoint union l Qed Lemma map disjoint union r 2 A m1 m2 m3 M A m1 m2 m1 m3 m1 m2 m3 Proof by rewrite map disjoint union r Qed Lemma insert union singleton l A m M A i x i x m i x m Proof apply map eq intros j apply option eq intros y rewrite lookup union Some raw destruct decide i j subst rewrite lookup singleton lookup insert intuition congruence rewrite lookup singleton ne lookup insert ne intuition congruence Qed Lemma insert union singleton r A m M A i x m i None i x m m i x Proof intro rewrite insert union singleton l map union commutative done by apply map disjoint singleton l Qed Lemma map disjoint insert l A m1 m2 M A i x i x m1 m2 m2 i None m1 m2 Proof rewrite insert union singleton l by rewrite map disjoint union l map disjoint singleton l Qed Lemma map disjoint insert r A m1 m2 M A i x m1 i x m2 m1 i None m1 m2 Proof rewrite insert union singleton l by rewrite map

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

  • Module fin_map_dom
    apply not elem of dom rewrite E solve elem of Qed Lemma dom alter A f m M A i dom D alter f i m dom D m Proof apply elem of equiv intros j rewrite elem of dom unfold is Some destruct decide i j simplify map equality eauto destruct m j naive solver Qed Lemma dom insert A m M A i x dom D i x m i dom D m Proof apply elem of equiv intros j rewrite elem of union elem of dom unfold is Some setoid rewrite lookup insert Some destruct decide i j esolve elem of Qed Lemma dom insert subseteq A m M A i x dom D m dom D i x m Proof rewrite dom insert solve elem of Qed Lemma dom insert subseteq compat l A m M A i x X X dom D m X dom D i x m Proof intros transitivity dom D m eauto using dom insert subseteq Qed Lemma dom singleton A i K x A dom D i x i Proof unfold singleton at 1 map singleton rewrite dom insert dom empty solve elem of Qed Lemma dom delete A m M A i dom D delete i m dom D m i Proof apply elem of equiv intros j rewrite elem of difference elem of dom unfold is Some setoid rewrite lookup delete Some esolve elem of Qed Lemma delete partial alter dom A m M A i f i dom D m delete i partial alter f i m m Proof rewrite not elem of dom apply delete partial alter Qed Lemma delete insert dom A m M A i x i dom D m delete i i x m m Proof rewrite not elem of dom apply delete insert Qed Lemma map disjoint dom A m1 m2 M A m1 m2 dom D m1 dom D m2 Proof rewrite map disjoint spec elem of equiv empty setoid rewrite elem of intersection setoid rewrite elem of dom unfold is Some naive solver Qed Lemma map disjoint dom 1 A m1 m2 M A m1 m2 dom D m1 dom D m2 Proof apply map disjoint dom Qed Lemma map disjoint dom 2 A m1 m2 M A dom D m1 dom D m2 m1 m2 Proof apply map disjoint dom Qed Lemma dom union A m1 m2 M A dom D m1 m2 dom D m1 dom D m2 Proof apply elem of equiv intros i rewrite elem of union elem of dom unfold is Some setoid rewrite lookup union Some raw destruct m1 i naive solver Qed Lemma dom intersection A m1 m2 M A dom D m1 m2 dom D m1 dom D m2 Proof apply elem of equiv intros i rewrite elem of intersection elem of dom unfold is Some setoid rewrite lookup intersection Some naive solver Qed Lemma dom difference A m1 m2 M A dom D m1 m2 dom D m1 dom D m2

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

  • Module mapset
    Instance mapset elem of dec x X mapset M unit Decision x X 1 Proof solve decision Defined Instance Collection K mapset M unit Proof split split unfold empty elem of mapset empty mapset elem of simpl intros by simpl map unfold singleton elem of mapset singleton mapset elem of simpl by split intros simplify map equality unfold union elem of mapset union mapset elem of intros m1 m2 simpl rewrite lookup union Some raw destruct m1 x as tauto unfold intersection elem of mapset intersection mapset elem of intros m1 m2 simpl rewrite lookup intersection Some assert is Some m2 x m2 x Some split eauto by intros naive solver unfold difference elem of mapset difference mapset elem of intros m1 m2 simpl rewrite lookup difference Some destruct m2 x as intuition congruence Qed Global Instance PartialOrder subseteq mapset M unit Proof split try apply intros apply mapset eq intuition Qed Global Instance FinCollection K mapset M unit Proof split apply unfold elements elem of at 2 mapset elems mapset elem of intros m x simpl rewrite elem of list fmap split intros y Hy subst by rewrite elem of map to list intros exists x by rewrite elem of map to list unfold elements mapset elems intros m simpl apply NoDup fst map to list Qed Definition mapset map with A B f bool A option B X mapset M unit M A M B let mX X in merge λ x y match x y with Some Some a f true a None Some a f false a None None end mX Definition mapset dom with A f A bool m M A mapset M unit Mapset merge λ x match x with Some a if f a then Some else None None None end m empty

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