Commit e3a5d03f authored by Robbert's avatar Robbert

Merge branch 'feature/binders' into 'master'

Proofs about binders

See merge request !83
parents aa051883 2883ab5a
Pipeline #19369 passed with stage
in 9 minutes and 55 seconds
...@@ -21,29 +21,50 @@ Instance binder_inhabited : Inhabited binder := populate BAnon. ...@@ -21,29 +21,50 @@ Instance binder_inhabited : Inhabited binder := populate BAnon.
Instance binder_countable : Countable binder. Instance binder_countable : Countable binder.
Proof. Proof.
refine (inj_countable' refine (inj_countable'
(λ mx, match mx with BAnon => None | BNamed x => Some x end) (λ b, match b with BAnon => None | BNamed s => Some s end)
(λ mx, match mx with None => BAnon | Some x => BNamed x end) _); by intros []. (λ b, match b with None => BAnon | Some s => BNamed s end) _); by intros [].
Qed. Qed.
(** The functions [cons_binder mx X] and [app_binder mxs X] are typically used (** The functions [cons_binder b ss] and [app_binder bs ss] are typically used
to collect the free variables of an expression. Here [X] is the current list of to collect the free variables of an expression. Here [ss] is the current list of
free variables, and [mx], respectively [mxs], are the binders that are being free variables, and [b], respectively [bs], are the binders that are being
added. *) added. *)
Definition cons_binder (mx : binder) (X : list string) : list string := Definition cons_binder (b : binder) (ss : list string) : list string :=
match mx with BAnon => X | BNamed x => x :: X end. match b with BAnon => ss | BNamed s => s :: ss end.
Infix ":b:" := cons_binder (at level 60, right associativity). Infix ":b:" := cons_binder (at level 60, right associativity).
Fixpoint app_binder (mxs : list binder) (X : list string) : list string := Fixpoint app_binder (bs : list binder) (ss : list string) : list string :=
match mxs with [] => X | b :: mxs => b :b: app_binder mxs X end. match bs with [] => ss | b :: bs => b :b: app_binder bs ss end.
Infix "+b+" := app_binder (at level 60, right associativity). Infix "+b+" := app_binder (at level 60, right associativity).
Instance set_unfold_cons_binder x mx X P : Instance set_unfold_cons_binder s b ss P :
SetUnfoldElemOf x X P SetUnfoldElemOf x (mx :b: X) (BNamed x = mx P). SetUnfoldElemOf s ss P SetUnfoldElemOf s (b :b: ss) (BNamed s = b P).
Proof. Proof.
constructor. rewrite <-(set_unfold (x X) P). constructor. rewrite <-(set_unfold (s ss) P).
destruct mx; simpl; rewrite ?elem_of_cons; naive_solver. destruct b; simpl; rewrite ?elem_of_cons; naive_solver.
Qed. Qed.
Instance set_unfold_app_binder x mxl X P : Instance set_unfold_app_binder s bs ss P Q :
SetUnfoldElemOf x X P SetUnfoldElemOf x (mxl +b+ X) (BNamed x mxl P). SetUnfoldElemOf (BNamed s) bs P SetUnfoldElemOf s ss Q
SetUnfoldElemOf s (bs +b+ ss) (P Q).
Proof. Proof.
constructor. rewrite <-(set_unfold (x X) P). induction mxl; set_solver. intros HinP HinQ.
constructor. rewrite <-(set_unfold (s ss) Q), <-(set_unfold (BNamed s bs) P).
clear HinP HinQ.
induction bs; set_solver.
Qed.
Lemma app_binder_named ss1 ss2 : (BNamed <$> ss1) +b+ ss2 = ss1 ++ ss2.
Proof. induction ss1; by f_equal/=. Qed.
Lemma app_binder_snoc bs s ss : bs +b+ (s :: ss) = (bs ++ [BNamed s]) +b+ ss.
Proof. induction bs; by f_equal/=. Qed.
Instance cons_binder_Permutation b : Proper ((≡ₚ) ==> (≡ₚ)) (cons_binder b).
Proof. intros ss1 ss2 Hss. destruct b; csimpl; by rewrite Hss. Qed.
Instance app_binder_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡ₚ)) app_binder.
Proof.
assert ( bs, Proper ((≡ₚ) ==> (≡ₚ)) (app_binder bs)).
{ induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
induction 1 as [|[]|[] []|]; intros ss1 ss2 Hss; simpl;
first [by eauto using perm_trans|by rewrite 1?perm_swap, Hss].
Qed. Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment