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 axiomatic_simple
    wand intro eauto rewrite assert Prop l by done eauto Qed Lemma ax assign r Γ δ A P Q Q ass e1 e2 μ γ τ p v va v Γ δ A ₑ emp e1 inl p emp Γ δ A ₑ P e2 inr v Q A Q A Γ δ assert assign p v ass τ va v A Q Γ δ p μ γ τ p μ perm lock γ freeze true va τ Q A Some Writable perm kind γ Γ δ A ₑ P e1 ass e2 inr v Q Proof intros rewrite left id A P eapply ax assign rewrite left id A eauto Qed Lemma ax eltl Γ δ A P Q e rs p p Γ δ A ₑ P e inl p Q A Q A Γ δ p rs inl p A Γ δ A ₑ P e rs inl p Q Proof rewrite commutative A intros eapply ax eltl eauto intros apply assert Prop intro l intros simplify equality apply assert exist intro with p assert and intro assert wand intro auto by rewrite assert Prop l by done Qed Lemma ax eltr Γ δ A P Q e rs v v Γ δ A ₑ P e inr v Q A Q A Γ δ v rs inr v A Γ δ A ₑ P e rs inr v Q Proof rewrite commutative A intros eapply ax eltr eauto intros apply assert Prop intro l intros simplify equality apply assert exist intro with v assert and intro assert wand intro auto by rewrite assert Prop l by done Qed Lemma ax insert Γ δ A P1 P2 Q1 Q2 e1 e2 r v1 v2 v Γ δ A ₑ P1 e1 inr v1 Q1 Γ δ A ₑ P2 e2 inr v2 Q2 A Q1 Q2 A Γ δ r v1 v2 inr v A Γ δ A ₑ P1 P2 r e1 e2 inr v Q1 Q2 Proof rewrite commutative A intros eapply ax insert eauto intros simpl rewrite associative A apply assert Prop intro l intros simplify equality rewrite commutative A Q2 associative A Q1 apply assert Prop intro r intros simplify equality apply assert exist intro with v assert and intro assert wand intro auto by rewrite assert Prop l by done Qed Lemma ax free Γ δ A P Q e o τ n τ p Γ δ A ₑ P e inl Ptr Addr o RArray 0 τ n 0 τ n τ τ p Ptr addr top o τ n true perm full τ n Q Γ δ A ₑ P free e inr voidV Q Proof intros eapply ax free with τ eauto intros apply assert Prop intro l intros simplify equality apply assert exist intro with o assert exist intro with n assert exist intro with τ p by rewrite assert Prop l by done Qed Lemma ax unop Γ δ A P Q op e v v

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


  • Module example_gcd
    solve elem of intros Hz apply ax stmt Prop pre try solve elem of intros Hy eapply ax if with intV uintT z B auto apply ax expr frame l rewrite assert singleton l var 1 at 1 apply ax expr exist pre intros a1 eapply ax expr weaken post by rewrite assert singleton l 2 Γ var 1 a1 exec by eapply assert exist intro assert eval int unop auto using assert memext r assert eval singleton r apply ax stmt Prop pre try solve elem of simpl intros apply ax local set R v var 0 false perm full uintT BT R v A set J l var 0 false perm full uintT BT J l A set T n var 0 false perm full uintT BT T n A set C mz var 0 false perm full uintT BT C mz A rewrite assert lift sep assert lift singleton simpl apply ax comp with var 0 false perm full intV uintT y mod z uintT var 1 μ1 γ1 intV uintT z uintT var 2 μ2 γ2 intV uintT y mod z uintT A eapply ax do with inr intV uintT y mod z by rewrite assert unlock sep assert lock singleton var 2 2 unlock indep rewrite assert singleton l var 0 assert exist sep apply ax expr exist pre intros a tmp eapply ax expr weaken post by rewrite assert singleton l 2 Γ var 0 a tmp rewrite associative A apply ax expr invariant l rewrite right id A assert singleton l var 1 assert exist sep A ptr assert sep exist A ptr apply ax expr exist pre intros a y eapply ax expr weaken post by rewrite assert singleton l 2 Γ var 1 a y rewrite associative A commutative A A rewrite associative A apply ax expr invariant l rewrite assert singleton l var 2 assert sep exist A ptr apply ax expr exist pre intros a z eapply ax expr weaken post by rewrite assert singleton l 2 Γ var 2 a z rewrite commutative A var 2 A associative A apply ax expr invariant r set A var 2 inl a z emp var 1 inl a y emp var 0 inl a tmp emp A rewrite associative A eapply ax assign r with a tmp false perm full intV uintT y mod z uintT a y μ1 γ1 intV uintT z uintT a z μ2 γ2 intV uintT z uintT A μ2 γ2 uintT T a z intV uintT y mod z try by exec eapply ax expr comma with a tmp false perm full intV uintT y mod z uintT a y μ1 γ1 intV uintT y uintT a z μ2 γ2 intV uintT z uintT A inr intV uintT y mod z eapply ax expr weaken post by rewrite assert unlock sep assert lock singleton a tmp 2 unlock indep by done apply ax expr invariant r set A a y μ1 γ1 intV uintT y

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

  • The CH₂O formalization
    structures option miscellaneous definitions and theorems on the option data type list miscellaneous definitions and theorems on lists vector miscellaneous definitions and theorems on vectors numbers miscellaneous facts on nat N and Z ars theorems and definitions on abstract rewriting systems collections definitions theorems and tactics for collections fin collections theorems on finite collections listset finite set implementation using unordered lists numbers generation of fresh numbers prelude exports all of

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


  • pfvr x pterm t pfvr y Proof with auto intros rewrite psubst intro with x x apply psubst pterm Qed Closed type annotated terms Inductive aterm atrm Prop aterm srt forall s aterm asrt s aterm fvr forall x A aterm A aterm afvr avr x A aterm bnd forall b t1 t2 L A aterm t1 aterm A forall x var x notin L aterm t2 afvr avr x A aterm abnd b t1 t2 aterm app forall t1 t2 aterm t1 aterm t2 aterm aapp t1 t2 Hint Constructors aterm Lemma sort exists aterm forall t aterm t exists s aterm asrt s Proof with auto induction 1 intros simpl in exists s Qed Lemma open rec aterm forall t k u aterm t t k u t Proof with auto intros gen k induction H intros simpl in unfold abnd unfold aapp f equal bnd unfold open in destruct var fresh L apply open rec term core with j 0 w afvr avr x A Qed Lemma asubst open rec forall t1 t2 u k x aterm u a x u k t2 t1 k a x u t2 a x u t1 Proof with auto induction t1 intros simpl simpl in f equal bvar case nat fvar case avar apply open rec aterm Qed Lemma asubst open forall t1 t2 u x aterm u a x u t1 t2 a x u t1 a x u t2 Proof with auto intros apply asubst open rec Qed Lemma asubst open var forall x y u t y aterm u a x u t fvr y a x u t fvr y Proof with auto intros rewrite asubst open simpl case avar Qed Lemma asubst fresh forall t u x x anotin afva t a x u t t Proof with auto intros induction t simpl in try solve f equal avardec auto fvr case avar induction x simpl in H avardec Qed Lemma asubst intro forall x t u x anotin afva t aterm u t u a x u t afvr x Proof with auto intros rewrite asubst open rewrite asubst fresh simpl case avar Qed Lemma asubst aterm forall t u x aterm t aterm u aterm a x u t Proof with auto intros induction H simpl fvar case avar bnd induction x apply aterm bnd with L v u L u fva a avr v t u t2 A A intros rewrite asubst open var apply H3 vardec intro injection H5 vardec Qed Lemma asubst avar aterm forall t x A A aterm t aterm A aterm a avr x A afvr avr x A t Proof with auto intros induction H simpl in case avar apply aterm bnd with L x u L A A0 intros rewrite asubst open var apply H3 vardec intro injection H5 vardec Qed Lemma open aterm forall t u L A aterm A forall x x notin L aterm t afvr avr x A aterm u aterm t u Proof with eauto intros destruct var fresh fva t u L rewrite asubst intro with x avr x A apply asubst aterm apply H0 vardec eapply notin fva afva vardec Qed Lemma open rec avar unique forall t1 t2 k x x anotin afva t1 x anotin afva t2 k afvr x t1 k afvr x t2 t1 t2 Proof with eauto intros gen k t2 induction t1 destruct t2 intros simpl in try repeat case nat try inversion H1 subst induction a simpl in H0 destruct H0 avardec induction x simpl in H destruct H avardec f equal eapply IHt1 1 try avardec eapply IHt1 2 try avardec f equal eapply IHt1 1 try avardec eapply IHt1 2 try avardec Qed Lemma open avar unique forall t1 t2 x x anotin afva t1 x anotin afva t2 t1 afvr x t2 afvr x t1 t2 Proof with eauto intros eapply open rec avar unique Qed Lemma close avar rec open forall x y z t1 i j i y i afvr y j afvr z close avar rec t1 j x j afvr z close avar rec i afvr y t1 j x Proof with auto induction t1 simpl intros bvr repeat try case nat simpl try case avar fvar repeat try case nat simpl try case avar bnd f equal app f equal Qed Lemma close avar open forall t x k aterm t t k fvr x close avar rec t k x Proof with auto intros gen k induction H simpl in intros unfold abnd in unfold aapp in f equal fvar induction x case avar simpl injection e intros subst case nat bnd induction x unfold open in destruct var fresh L u v u fva t2 u fva S k fvr avr v t close avar rec t2 S k avr v t apply open rec avar unique with k 0 x avr x A intros try solve eapply notin fva afva vardec rewrite close avar rec open apply H2 vardec intro injection H3 vardec Qed Lemma close avar fresh forall x t k x anotin afva close avar rec t k x Proof with auto induction t intros simpl in try avardec case avar simpl avardec rewrite AvarsP notin union split rewrite AvarsP notin union split Qed Lemma shape rec aterm forall t x k aterm t exists s t k afvr x s x anotin afva s Proof with auto intros exists close avar rec t k x split apply close avar open apply close avar fresh Qed Lemma shape aterm forall t x aterm t exists s t s afvr x x anotin afva s Proof with auto intros apply shape rec aterm Qed Lemma aterm rename forall x y t A aterm A x notin fva t aterm t afvr avr x A aterm t afvr avr y A Proof with auto intros rewrite asubst intro with x avr x A apply asubst aterm eapply notin fva afva Qed Hereditary free variable substitution Section hsubst def Variable f avar avar atrm avar Fixpoint hsubst t atrm z avar u atrm struct t atrm match t with srt s asrt s bvr n abvr n fvr v if v a z then u else afvr f v z u bnd b t1 t2 abnd b hsubst t1 z u hsubst t2 z u app t1 t2 aapp hsubst t1 z u hsubst t2 z u end End hsubst def Fixpoint avar hsubst v avar z avar u atrm struct v avar match v with avr x t avr x hsubst avar hsubst t z u end Definition hsubst t atrm z avar u atrm atrm hsubst avar hsubst t z u Notation h z u t hsubst t z u at level 68 Lemma hsubst eq var forall x u h x u afvr x u Proof with auto intros simpl case avar Qed Lemma hsubst open rec forall t1 t2 u k x aterm u h x u k t2 t1 k h x u t2 h x u t1 Proof with auto induction t1 intros simpl in unfold abnd in unfold aapp in f equal bvar case nat fvar case avar apply open rec aterm Qed Lemma hsubst open forall t1 t2 u x aterm u h x u t1 t2 h x u t1 h x u t2 Proof with auto intros apply hsubst open rec Qed Lemma hsubst fresh forall t u x x anotin ahfv t h x u t t Proof with auto intros induction t using atrm rec2 with P fun v x anotin avar ahfv v afvr avar hsubst v x u fvr v simpl in unfold abnd in unfold aapp in unfold afvr in repeat f equal case avar destruct x as y B simpl in avardec apply IHt1 avardec apply IHt2 avardec apply IHt1 avardec apply IHt2 avardec apply IHt avardec Qed Lemma hsubst intro forall x t u x anotin ahfv t aterm u t u h x u t afvr x Proof with auto intros rewrite hsubst open rewrite hsubst fresh simpl case avar Qed Lemma hsubst open var forall x v A u t avr v A aterm u h x u t afvr avr v h x u A h x u t fvr avr v A Proof with auto intros rewrite hsubst open simpl case avar Qed Lemma hsubst aterm forall t u x aterm t aterm u aterm h x u t Proof with auto intros induction H simpl fvar case avar bnd induction x apply aterm bnd with L L u v A h avr v t u A intros rewrite hsubst open var apply H3 vardec intro injection H5 intros vardec Qed Non overlapping beta reduction of pterms Inductive pbeta ptrm ptrm Prop pbeta red forall t1 t2 u pterm pbnd abs t1 t2 pterm u pbeta papp pbnd abs t1 t2 u t2 u pbeta app forall t1 t1 t2 t2 pbeta t1 t1 pbeta t2 t2 pbeta papp t1 t2 papp t1 t2 pbeta bnd forall b t1 t1 t2 t2 L pbeta t1 t1 forall x x notin L pbeta t2 pfvr x t2 pfvr x pbeta pbnd b t1 t2 pbnd b t1 t2 Hint Constructors pbeta Notation A p B pbeta A B at level 80 Lemma pbeta pterm forall t t t p t pterm t pterm t Proof with auto intros split induction H red inversion clear H destruct var fresh L eapply open pterm Qed Lemma psubst pbeta forall t t u x t p t pterm u p x u t p p x u t Proof with auto intros induction H simpl red rewrite psubst open apply pbeta red change pterm p x u pbnd abs t1 t2 apply psubst pterm apply psubst pterm bnd apply pbeta bnd with L L u x intros repeat rewrite psubst open var try vardec apply H2 vardec Qed Lemma pbeta rename forall x y t1 t2 x notin fv t1 x notin fv t2 t1 pfvr x p t2 pfvr x t1 pfvr y p t2 pfvr y Proof with auto intros rewrite psubst intro with x x t t1 rewrite psubst intro with x x t t2 apply psubst pbeta Qed Non overlapping beta reduction of aterms Inductive abeta atrm atrm Prop abeta red forall t1 t2 u aterm bnd abs t1 t2 aterm u abeta app bnd abs t1 t2 u t2 u abeta app forall t1 t1 t2 t2 abeta t1 t1 abeta t2 t2 abeta app t1 t2 app t1 t2 abeta bnd forall b t1 t1 t2 t2 L A abeta t1 t1 aterm A forall x x notin L abeta t2 afvr avr x A t2 afvr avr x A abeta bnd b t1 t2 bnd b t1 t2 Hint Constructors abeta Notation A a B abeta A B at level 80 Lemma abeta aterm forall t t t a t aterm t aterm t Proof with auto intros induction H split decompose ands red inversion clear H apply open aterm with A A L L bnd apply aterm bnd with L L A A intros eapply H2 apply aterm bnd with L L A A intros apply open aterm with L L A A intros eapply H2 Qed Lemma asubst abeta forall t t u x t a t aterm u a x u t a a x u t Proof with auto intros induction H simpl red rewrite asubst open apply abeta red change aterm a x u abnd abs t1 t2 apply asubst aterm apply asubst aterm bnd induction x as x B apply abeta bnd with L L u x A A intros repeat rewrite asubst open var apply H3 vardec intro injection H5 vardec intro injection H5 vardec Qed Lemma hsubst abeta forall t t u x t a t aterm u h x u t a h x u t Proof with auto intros induction H simpl red rewrite hsubst open apply abeta red change aterm h x u abnd abs t1 t2 apply hsubst aterm apply hsubst aterm bnd induction x as x B apply abeta bnd with L L u x A h avr x B u A intros apply hsubst aterm repeat rewrite hsubst open var apply H3 vardec intro injection H5 vardec intro injection H5 vardec Qed Lemma abeta rename forall x y t1 t2 A aterm A avr x A anotin afva t1 avr x A anotin afva t2 t1 afvr avr x A a t2 afvr avr x A t1 afvr avr y A a t2 afvr avr y A Proof with auto intros rewrite asubst intro with x avr x A t t1 rewrite asubst intro with x avr x A t t2 apply asubst abeta Qed Reflexive symmetric transitive closure Inductive equiv A Set S A Prop R A A Prop rs forall a1 a2 A R a1 a2 S a1 S a2 A A Prop equiv refl forall t S t equiv S R rs t t equiv sym forall t t equiv S R rs t t equiv S R rs t t equiv trans forall t2 t1 t3 equiv S R rs t1 t2 equiv S R rs t2 t3 equiv S R rs t1 t3 equiv step forall t t R t t equiv S R rs t t Hint Constructors equiv Lemma equiv S forall A Set S R rs t1 t2 A equiv A S R rs t1 t2 S t1 S t2 Proof with auto intros induction H split apply rs t t H apply rs t t H Qed Beta conversion Notation A pbeta B equiv pterm pbeta pbeta pterm A B at level 80 Notation A abeta B equiv aterm abeta abeta aterm A B at level 80 Lemma pbeta equiv pterm forall t1 t2 t1 pbeta t2 pterm t1 pterm t2 Proof apply equiv S Qed Lemma abeta equiv aterm forall t1 t2 t1 abeta t2 aterm t1 aterm t2 Proof apply equiv S Qed Lemma psubst pbeta equiv forall t t u x t pbeta t pterm u p x u t pbeta p x u t Proof with auto intros induction H simpl refl apply equiv refl apply psubst pterm trans auto step apply equiv step apply psubst pbeta Qed Lemma asubst abeta equiv forall t t u x t abeta t aterm u a x u t abeta a x u t Proof with auto intros induction H simpl refl apply equiv refl apply asubst aterm trans auto step apply equiv step apply asubst abeta Qed Lemma hsubst abeta equiv forall t t u x t abeta t aterm u h x u t abeta h x u t Proof with auto intros induction H simpl refl apply equiv refl apply hsubst aterm trans auto step apply equiv step apply hsubst abeta Qed Environments Definition env list pvar ptrm Fixpoint get x pvar E env struct E option ptrm match E with nil None y A E if x y then Some A else get x E end Definition binds x A E get x E Some A Fixpoint dom E env vars match E with nil x E x u dom E end Inductive ok env Prop ok nil ok nil ok cons forall E x A x notin dom E ok E ok x A E Hint Constructors ok Fixpoint after x pvar E env struct E env match E with nil nil y E if x y then E else after x E end Fixpoint before x pvar E env struct E env match E with nil nil y A E if x y then nil else y A before x E end Lemma dom get some forall E env x x in dom E exists A get x E Some A Proof with auto split intros induction E vardec destruct a simpl in case var eexists apply IHE vardec inversion clear H inversion H0 destruct a simpl in case var vardec specialize IHE H vardec Qed Lemma dom get none forall E env x x notin dom E get x E None Proof with auto split intros induction E destruct a simpl in case var vardec apply IHE vardec simpl vardec destruct a simpl in case var discriminate specialize IHE H vardec Qed Lemma dom binds forall E env x x in dom E exists A binds x A E Proof unfold binds apply dom get some Qed Lemma in dom concat forall E F x x in dom E u dom F x in dom E F Proof with auto split induction E simpl in intros vardec induction a vardec vardec induction a vardec Qed Lemma notin dom concat forall E F x x notin dom E x notin dom F x notin dom E F Proof with auto split intros rewrite ok E ok F Proof with auto induction E intros simpl in split destruct a as y B inversion clear H apply ok cons apply proj2 notin dom concat E F y H0 specialize IHE F H1 auto destruct a as y B inversion clear H specialize IHE F H1 auto Qed Lemma dom middle forall E F G x x in dom E G ok E F G x notin dom F Proof with auto intros assert x in dom E x in dom G apply Vars union 1 eapply in dom concat destruct H1 x in dom E rewrite x in dom E x A F Proof with auto induction E simpl intros vardec inversion clear H destruct a as y B apply Vars union 3 Qed Lemma binds middle forall x A E F ok E x A F binds x A E x A F Proof with auto induction E unfold binds in simpl intros case var auto destruct a as y B simpl in case var inversion clear H destruct H0 apply ok middle inversion clear H Qed Lemma binds middle2 forall x A B E F ok E x B F binds x A E x B F A B Proof with auto induction E unfold binds in simpl intros case var injection H0 auto destruct a as y C inversion clear H case var destruct H1 apply ok middle eapply IHE auto Qed Lemma binds unique forall E env x A1 A2 binds x A1 E binds x A2 E A1 A2 Proof with eauto intros unfold binds in rewrite H in H0 injection H0 Qed Lemma binds nil forall x A binds x A nil Proof unfold binds simpl intros discriminate Qed Lemma binds cons forall x A E binds x A x A E Proof with auto intros unfold binds simpl case var Qed Lemma binds cons2 forall x A y B E x binds x A E binds x A y B E Proof with auto unfold binds intros simpl case var Qed Lemma binds first forall x A A E binds x A x A E A A Proof with auto unfold binds intros simpl in case var injection H Qed Lemma binds append forall x A E F binds x A F ok E F binds x A E F Proof with auto induction E intros simpl in destruct a as y B unfold binds simpl in case var inversion clear H0 destruct H1 eapply in dom concat apply Vars union 3 eapply dom binds exists A inversion clear H0 unfold binds in Qed Lemma binds append tail forall x A E F binds x A E binds x A E F Proof with auto induction E intros simpl in eelim binds nil auto unfold binds in destruct a as y B simpl in case var Qed Lemma binds weaken forall x A E F G binds x A E G ok E F G binds x A E F G Proof with auto intros induction E simpl in apply binds append destruct a as y B unfold binds in simpl case var inversion clear H case var auto simpl in case var auto apply IHE inversion clear H0 Qed Lemma binds weak forall x A F G binds x A G ok F G binds x A F G Proof with auto intros rewrite app nil apply binds weaken Qed Lemma binds concat forall E F x A ok E F binds x A E F binds x A E x binds x A F Proof with auto induction E simpl in intros right split apply binds nil destruct a as y B inversion clear H unfold binds in simpl in case var left split intro destruct H1 eapply in dom concat apply Vars union 3 eapply dom get some exists A Qed Lemma before after forall E x A binds x A E E before x E x A after x E Proof with auto induction E intros simpl in edestruct binds nil auto destruct a as y B case var simpl in unfold binds in H simpl in H case var injection H intros subst auto f equal apply IHE unfold binds in H simpl in H case var auto Qed Lemma after concat forall E F x x in dom E after x E F after x E F Proof with auto induction E simpl in intros vardec destruct a as y B case var destruct Vars union 1 H vardec Qed Lemma after concat2 forall E F x x notin dom E after x E F after x F Proof with auto induction E simpl in intros vardec destruct a as y B case var vardec apply IHE vardec Qed Lemma after middle forall E F x A ok E x A F after x E x A F F Proof with auto induction E intros simpl in case var auto destruct a as y B inversion clear H case var destruct H0 eapply in dom concat apply Vars union 3 simpl vardec Qed Properties on environments Definition env prop P ptrm Prop E env forall x A binds x A E P A Lemma env prop nil forall P ptrm Prop env prop P nil Proof unfold env prop intros inversion H Qed Lemma env prop cons forall P ptrm Prop A E x P A env prop P E env prop P x A E Proof with eauto unfold env prop unfold binds intros simpl in H1 case var inversion H1 subst A0 eapply H0 Qed Definition env exists P ptrm Prop E env exists x exists A binds x A E P A Definition env sseq E F forall x A binds x A E binds x A F Lemma env exists nil forall P ptrm Prop env exists P nil Proof unfold env exists intros P inversion clear H inversion clear H0 decompose ands edestruct binds nil auto Qed Lemma env exists cons forall P ptrm Prop A E x env exists P x A E P A env exists P E Proof with eauto unfold env exists unfold binds intros inversion clear H inversion clear H0 simpl in H case var decompose ands injection H0 intros subst right repeat eexists Qed Sub environments Notation E x A E E E nil Proof with auto intros induction E destruct a as x A unfold env sseq in eelim binds nil apply H apply binds cons Qed Substitution on environments Fixpoint env map f ptrm ptrm E env struct E env match E with nil nil x A E x f A env map f E end Lemma env map binds forall x A f E binds x A E binds x f A env map f E Proof with auto unfold binds induction E simpl in intros discriminate destruct a as y B case var simpl case var repeat f equal injection H auto case var auto Qed Lemma env map cons forall E f x A x f A env map f E env map f x A E Proof simpl auto Qed Lemma env map dom forall E f dom E dom env map f E Proof with auto split induction E intros simpl in destruct a0 as x A simpl in vardec destruct a0 as x A simpl in vardec Qed Definition esubst E z u env map fun A p z u A E Notation e z u E esubst E z u at level 68 Lemma esubst binds forall x A E z u binds x A E binds x p z u A e z u E Proof with auto intros change binds x fun A0 p z u A0 A e z u E apply env map binds Qed Lemma esubst cons forall E x A y u x p y u A e y u E e y u x A E Proof intros change x fun A0 p y u A0 A e y u E e y u x A E apply env map cons Qed Translation from ptrms to atrms Fixpoint atp t atrm struct t ptrm match t with srt s psrt s bvr n pbvr n fvr avr x a pfvr x bnd b t1 t2 pbnd b atp t1 atp t2 app t1 t2 papp atp t1 atp t2 end Lemma atp open rec forall t atrm k nat u atrm atp k u t k atp u atp t Proof with auto induction t intros simpl bvr case nat afvr induction v simpl bnd rewrite IHt1 rewrite IHt2 app rewrite IHt1 rewrite IHt2 Qed Lemma atp open forall t u atp t u atp t atp u Proof intros unfold open apply atp open rec Qed Lemma aterm imp pterm forall t aterm t pterm atp t Proof with eauto intros induction H simpl bnd eapply pterm bnd with L L intros cut pterm atp t2 afvr avr x A intros rewrite atp open in H4 simpl in H3 Qed Translation from ptrms to atrms Inductive pta env ptrm atrm Prop pta srt forall E s pta wde E pta E psrt s asrt s pta fvr forall E A A x pta wde E binds x A E pta E A A pta E pfvr x afvr avr x A pta bnd forall E b t1 t1 t2 t2 L pta E t1 t1 forall x s x notin L pta x psrt s E t2 pfvr x t2 afvr avr x asrt s pta E pbnd b t1 t2 abnd b t1 t2 pta app forall E t1 t1 t2 t2 pta E t1 t1 pta E t2 t2 pta E papp t1 t2 aapp t1 t2 with pta wde env Prop pta wde nil pta wde nil pta wde cons forall E x A A x notin dom E pta E A A pta wde E pta wde x A E Scheme pta ind2 Induction for pta Sort Prop with pta wde ind2 Induction for pta wde Sort Prop Hint Constructors pta pta wde Lemma sort exists pta forall E t t pta E t t exists s pta E psrt s asrt s Proof with auto induction 1 intros exists s Qed Lemma pta wde weak forall E F pta wde E F pta wde F Proof with auto induction E simpl in intros inversion clear H Qed Lemma pta unique forall E t t1 t2 pta E t t1 pta E t t2 t1 t2 Proof with eauto intros gen t2 induction H intros srt inversion clear H0 fvr inversion clear H2 repeat f equal apply IHpta assert A A0 eapply binds unique subst bnd inversion clear H2 f equal specialize IHpta t1 0 H3 subst edestruct sort exists pta as s destruct var fresh L0 u L u fva t2 u fva t2 0 as x0 F apply open avar unique with x avr x0 asrt s intros try solve eapply notin fva afva vardec eapply H1 vardec eapply H4 vardec app inversion clear H1 f equal Qed Lemma pta injective forall E t t1 t2 pta E t1 t pta E t2 t t1 t2 Proof with eauto intros gen t2 induction H intros srt inversion clear H0 fvr inversion clear H2 bnd inversion clear H2 f equal assert t1 t3 subst edestruct sort exists pta as s destruct var fresh L0 u L u fv t2 u fv t4 as x0 F apply open var unique with x x0 intros try vardec eapply H1 with s s vardec eapply H4 vardec app inversion clear H1 f equal Qed Lemma pta term forall E t t pta E t t pterm t aterm t Proof with auto intros induction H repeat split decompose ands destruct sort exists aterm with t t1 as s apply pterm bnd with L L intros eapply H1 x s destruct sort exists aterm with t t1 as s apply aterm bnd with L L A asrt s intros eapply H1 Qed Lemma pta wd env forall E t t pta E t t pta wde E Proof induction 1 auto Qed Lemma pta env ok forall E pta wde E ok E Proof induction 1 auto Qed Lemma pta weaken forall E F G env t t pta E G t t pta wde E F G pta E F G t t Proof with auto intros dependent induction H fvar apply pta fvr with A A apply binds weaken apply pta env ok bnd apply pta bnd with L L u dom E0 F G intros rewrite app comm cons apply H1 vardec rewrite pta wde F G pta F G t t Proof with auto intros rewrite app nil with l F G apply pta weaken Qed Lemma pta weak single forall G x A t t pta G t t pta wde x A G pta x A G t t Proof with auto intros rewrite app single apply pta weak Qed Lemma pta wde binds after forall E x A pta wde E binds x A E exists A pta after x E A A Proof with auto induction 1 intros edestruct binds nil unfold binds in simpl in case var injection H2 intros subst Qed Lemma pta wde binds forall E x A pta wde E binds x A E exists A pta E A A Proof with auto intros destruct pta wde binds after E x A as A exists A rewrite before after E x A in H rewrite app single in H rewrite ass app in H apply pta weak Qed Lemma pta env concat forall E F pta wde E pta wde F forall x x in dom E x notin dom F pta wde E F Proof with auto induction E intros simpl in destruct a as x A inversion clear H apply pta wde cons with A A eapply notin dom concat E F split eapply H1 vardec rewrite app nil end with l E F rewrite app ass eapply pta weaken rewrite x in fv t x in hfv t x in dom E Proof with auto intros induction H simpl in srt vardec fvr destruct x x0 subst eapply dom binds exists A apply IHpta vardec bnd destruct var fresh L u x decompose or H0 destruct Vars union 1 H3 edestruct sort exists pta as s assert x in x0 u dom E apply H2 with s s vardec left apply open fv2 vardec edestruct sort exists pta as s assert x in x0 u dom E apply H2 with s s vardec right apply open hfv2 vardec app decompose or H0 destruct Vars union 1 H2 Qed Lemma notin pta fv forall E env t t x pta E t t x notin dom E x notin fv t x notin hfv t Proof with auto split intro destruct H0 eapply pta fv intro destruct H0 eapply pta fv Qed Lemma notin pta fv dom forall E x pta wde E x notin dom E env prop fun C x notin fv C E Proof with auto induction E intros apply env prop nil destruct a as y B inversion clear H simpl in H0 apply env prop cons eapply notin pta fv vardec apply IHE vardec Qed Lemma pta fv fva forall E t t pta E t t fv t fva t Proof with auto intros split gen a induction H intros simpl in destruct Vars union 1 H2 apply Vars union 2 apply Vars union 3 destruct var fresh L u a edestruct sort exists pta as s auto assert a in fva t2 u fva afvr avr x asrt s apply open fva1 apply H1 vardec apply open fv2 simpl in vardec destruct Vars union 1 H1 apply Vars union 2 apply Vars union 3 destruct Vars union 1 H2 apply Vars union 2 apply Vars union 3 destruct var fresh L u a assert a in fv t2 u fv pfvr x apply open fv1 edestruct sort exists pta as s auto apply H1 with s s vardec apply open fva2 simpl in vardec destruct Vars union 1 H1 apply Vars union 2 apply Vars union 3 Qed Lemma notin pta fv type forall E t t x A A pta E A A binds x A E pta E t t env prop fun B x notin fv B E avr x A anotin ahfv type t Proof with auto intros gen x induction H1 intros simpl in srt avardec fvr eapply AvarsP eq notin apply afva union ahfv type eapply AvarsP notin union split eapply notin fva afva eapply VarsP eq notin apply VarsP P equal sym eapply pta fv fva apply H2 unfold env prop in H4 apply H4 x auto bnd eapply AvarsP notin union split auto destruct var fresh L u dom E u x as y edestruct sort exists pta as s auto eapply open notin ahfv type2 eapply H2 with s s x y vardec apply pta weak single assert pta wde E eapply pta wd env auto apply pta wde cons with A asrt s vardec apply binds cons2 vardec apply env prop cons simpl vardec app eapply AvarsP notin union auto Qed Lemma pta notin hfv type forall E x A A t1 t2 pta E A A pta x A E t1 t2 avr x A anotin ahfv type t2 Proof with auto intros assert H1 pta wd env H0 inversion clear H1 apply notin pta fv type with E x A E t t1 A A apply pta weak single apply pta wde cons with A A apply binds cons apply env prop cons eapply notin pta fv auto apply notin pta fv dom Qed Lemma pta subst forall E F t t u u x A A pta F A A pta E x A F t t pta F u u pta e x u E F p x u t h avr x A u t Proof with auto intros gen eq E x A F as G gen E induction H0 using pta ind2 with P0 fun G W pta wde G forall E G E x A F pta wde e x u E F intros simpl in subst srt auto fvar case var x x0 case avar x x0 A 0 A apply pta weak x x0 A 0 x0 case avar destruct n injection e clear n0 rename E0 into E rename x0 into y rename A0 into B rename A 0 into B specialize IHpta E refl equal E x A F specialize IHpta0 E refl equal E x A F edestruct binds concat E x A F apply pta env ok apply b binds y B E decompose ands apply pta fvr with A p x u B apply binds append tail apply esubst binds binds

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

  • Module finite
    y apply card 0 inv HA y destruct finite surjective A B as g auto with lia destruct surjective cancel g as f exists f apply cancel injective intros f unfold card rewrite fmap length f by apply contains length finite injective contains f Qed Lemma finite bijective A Finite A B Finite B card A card B f A B Injective f Surjective f Proof split intros destruct proj1 finite injective A B as f auto with lia exists f auto using finite injective surjective f intros f apply anti symmetric apply finite injective by exists f destruct surjective cancel f as g eauto using cancel injective Qed Lemma injective card Finite A Finite B f A B Injective f card A card B Proof apply finite injective eauto Qed Lemma surjective card Finite A Finite B f A B Surjective f card B card A Proof destruct surjective cancel f as g apply injective card with g cancel injective Qed Lemma bijective card Finite A Finite B f A B Injective f Surjective f card A card B Proof apply finite bijective eauto Qed Decidability of quantification over finite types Section forall exists Context Finite A P A Prop x Decision P x Lemma Forall finite Forall P enum A x P x Proof rewrite Forall forall intuition auto using elem of enum Qed Lemma Exists finite Exists P enum A x P x Proof rewrite Exists exists naive solver eauto using elem of enum Qed Global Instance forall dec Decision x P x Proof refine cast if decide Forall P enum A abstract by rewrite Forall finite Defined Global Instance exists dec Decision x P x Proof refine cast if decide Exists P enum A abstract by rewrite Exists finite Defined End forall exists Instances Section enc finite Context x y A Decision x y Context to nat A nat of nat nat A c nat Context of to nat x of nat to nat x x Context to nat c x to nat x c Context to of nat i i c to nat of nat i i Program Instance enc finite Finite A enum of nat seq 0 c Next Obligation apply NoDup alt intros i j x rewrite list lookup fmap intros Hi Hj destruct seq i as i eqn Hi seq j as j eqn Hj simplify equality destruct lookup seq inv Hi lookup seq inv Hj subst rewrite to of nat i to of nat j by done by f equal Qed Next Obligation intros x rewrite elem of list fmap exists to nat x split auto by apply elem of list lookup 2 with to nat x lookup seq Qed Lemma enc finite card card A c Proof unfold card simpl by rewrite fmap length seq length Qed End enc finite Section bijective finite Context Finite A x y B Decision x y f A B g B A Context Injective f Cancel f g Program Instance bijective finite Finite B

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

  • Module lexico
    po Lexico A Lexico B StrictOrder lexico A StrictOrder lexico B StrictOrder lexico A B Proof split intros x y apply prod lexico irreflexive by apply irreflexivity lexico y intros eapply prod lexico transitive eauto apply transitivity Qed Instance prod lexico trichotomyT Lexico A tA TrichotomyT lexico A Lexico B tB TrichotomyT lexico B TrichotomyT lexico A B Proof red refine λ p1 p2 match trichotomyT lexico p1 1 p2 1 with inleft left inleft left inleft right cast trichotomy trichotomyT lexico p1 2 p2 2 inright inright end clear tA tB abstract unfold lexico prod lexico auto using injective projections Defined Instance bool lexico po StrictOrder lexico bool Proof split by intros by intros Qed Instance bool lexico trichotomy TrichotomyT lexico bool Proof red refine λ b1 b2 match b1 b2 with false false inleft right false true inleft left true false inright true true inleft right end abstract unfold strict lexico bool lexico naive solver Defined Instance nat lexico po StrictOrder lexico nat Proof unfold lexico nat lexico apply Qed Instance nat lexico trichotomy TrichotomyT lexico nat Proof red refine λ n1 n2 match Nat compare n1 n2 as c return Nat compare n1 n2 c with Lt λ H inleft left nat compare Lt lt H Eq λ H inleft right nat compare eq H Gt λ H inright nat compare Gt gt H end eq refl Defined Instance N lexico po StrictOrder lexico N Proof unfold lexico N lexico apply Qed Instance N lexico trichotomy TrichotomyT lexico N Proof red refine λ n1 n2 match N compare n1 n2 as c return N compare n1 n2 c with Lt λ H inleft left proj2 N compare lt iff H Eq λ H inleft right N compare eq H Gt λ H inright proj1 N compare gt

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

  • Module pretty
    x N go y y x N string string s string string match decide 0 x N with left H go x div 10 N N div lt x 10 H eq refl String pretty N char x mod 10 s right s end Instance pretty N Pretty N λ x Fix F pretty N go wf guard 32 N lt wf 0 x string Instance pretty N injective Injective eq N pretty Proof assert x y x 10 y 10 pretty N char x pretty N char y x y N compute intros by repeat discriminate case match set f x acc Acc x Fix F pretty N go acc cut x acc y acc s s length s length s f x acc s f y acc s x y s s intros help x y eapply help eauto assert x acc s length f x acc s length s as help setoid rewrite Nat le ngt fix 2 intros x s simpl unfold pretty N go fold pretty N go destruct decide 0 x N auto etransitivity eauto simpl lia fix 2 intros x y s s simpl unfold pretty N go fold pretty N go intros

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

  • Module natural_type_environment
    τ s Γ1 Γ1 τ s Γ1 Γ2 natural fields align Γ1 τ s natural fields align Γ2 τ s Proof intros H τ s unfold natural fields align induction H τ s simpl auto using natural align of weaken Qed Lemma natural field sizes weaken rec1 rec2 Γ1 Γ2 whole align pos τ s Γ1 Γ1 Γ2 Γ1 τ s Forall λ τ rec1 τ rec2 τ τ s natural field sizes rec1 Γ1 whole align pos τ s natural field sizes rec2 Γ2 whole align pos τ s Proof intros H τ s Hrec revert pos H τ s induction Hrec as τ τ s H τ IH intros decompose Forall simpl auto rewrite H τ IH by done destruct τ s as τ2 τ s simpl done decompose Forall by erewrite natural align of weaken by eauto Qed Lemma natural size of compound proper Γ1 Γ2 rec1 rec2 c t τ s let fc Γ rec c t tag τ s match c with Struct kind sum list natural field sizes rec Γ natural fields align Γ τ s 0 τ s Union kind let sz foldr max 1 rec τ s in sz natural padding sz natural fields align Γ τ s end in Γ1 Γ1 Γ2 Γ1 t Some τ s Γ1 τ s Forall λ τ rec1 τ rec2 τ τ s fc Γ1 rec1 c t τ s fc Γ2 rec2 c t τ s Proof intros fc destruct c simpl intros H τ s Hrec erewrite natural fields align weaken by eauto by erewrite natural field sizes weaken by eauto intros by erewrite Forall fmap ext 1 natural fields align weaken by eauto Qed Lemma natural size of base Γ τ b size of Γ baseT τ b match τ b with voidT 1 intT τ i rank size rank τ i τ p ptr size τ p end BT Proof done Qed Lemma natural size of array Γ τ n size of Γ τ n n size of Γ τ Proof unfold size of simpl by apply type iter array Qed Lemma natural size of compound Γ c t τ s Γ Γ t Some τ s size of Γ compoundT c t match c with Struct kind sum list field sizes Γ τ s Union kind let sz foldr max 1 size of Γ τ s in sz natural padding sz natural fields align Γ τ s end Proof intros unfold size of simpl unfold natural size of by rewrite type iter compound by eauto using natural size of compound proper with typeclass instances Qed Lemma natural size of weaken Γ1 Γ2 τ Γ1 Γ1 τ Γ1 Γ2 size of Γ1 τ size of Γ2 τ Proof intros unfold size of simpl unfold natural size of apply type iter weaken eauto using natural size of compound proper with typeclass instances Qed Lemma natural align ne 0 Γ τ Γ Γ τ align of Γ τ 0 Proof intros H Γ

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