Commit fcad5dc2 authored by charguer's avatar charguer

substn new definition

parent b8db9790
......@@ -29,7 +29,7 @@ Lemma Rule_apply : forall (f:func) `{EA:Enc A} (x:A),
Triple (val_apply ``f ``x) H Q.
Proof using.
introv M. xcf. (* todo why not simplified? *)
unfold Substs; simpl; rew_enc_dyn.
unfold Substn, substn; simpl; rew_enc_dyn.
xapp. hsimpl~.
Qed.
......
......@@ -298,13 +298,13 @@ Definition val_mlist_copy :=
Lemma Rule_mlist_copy : forall p (L:list int),
Triple (val_mlist_copy ``p)
PRE (p ~> MList L)
POST (fun (p':loc) =>
POST (fun (p':loc) =>
(p ~> MList L) \* (p' ~> MList L)).
Proof using.
intros. gen p. induction_wf IH: list_sub_wf L. xcf.
xapps~. xif ;=> C.
{ xval. subst p. rewrite MList_null_eq. hsimpl~. }
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p1 T1 E.
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p1 T1 E.
subst. xapps. xapps. xapp~ as p1'. xapp.
intros p'. do 2 rewrite MList_cons_eq. hsimpl. }
Qed.
......@@ -485,7 +485,7 @@ Lemma Rule_mlist_length_using_iter : forall A `{EA:Enc A} (L:list A) (p:loc),
Proof using.
xcf. xapps ;=> R. xval ;=> F HF.
xapp (@Rule_mlist_iter _ _ (fun (K:list A) => R ~~> length K)).
{ intros x K. xcf. unfold Substs; simpl. (* todo: Unfold *)
{ intros x K. xcf. unfold Substn, substn; simpl. (* todo: Unfold *)
xapp. hsimpl. rew_list; math. }
xapps ;=> r Hr. hsimpl~.
Qed.
......
......@@ -24,7 +24,7 @@ Implicit Types v : val.
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
F = (val_funs xs t1) ->
var_funs (length Vs) xs ->
triple (substs xs Vs t1) H Q ->
triple (substn xs Vs t1) H Q ->
triple (trm_apps F Vs) H Q.
Proof using.
introv E N M. intros h1 h2 D H1.
......@@ -108,7 +108,7 @@ Hint Resolve Normal_hsingle.
Tactic Notation "xdef" :=
rew_nary; rew_vals_to_trms;
match goal with |- triple (trm_apps (trm_val ?f) _) _ _ =>
match goal with |- triple (trm_apps (trm_val ?f) _) _ _ =>
applys rule_apps_funs;
[unfold f; rew_nary; reflexivity | auto | simpl]
end.
......@@ -133,17 +133,17 @@ Proof using.
introv M. xdef. xchange (@RO_himpl_RO_hstar_RO (p ~~~> v)).
rew_heap. applys rule_let (RO (p ~~~> v)).
{ applys rule_get_ro. }
{ intros x; simpl. xpull ;=> E. subst x.
{ intros x; simpl. xpull ;=> E. subst x.
applys rule_consequence M; hsimpl. }
Qed.
(* Note: this specification allows [f] to call [val_get] on [r],
as illustrated next
(* Note: this specification allows [f] to call [val_get] on [r],
as illustrated next
Definition val_demo_1 :=
ValFun 'n :=
Let 'p := val_ref 'n in
LetFun 'f 'x :=
LetFun 'f 'x :=
Let 'y := val_get 'p in
val_add 'x 'y in
val_ref_apply 'f 'p.
......@@ -169,7 +169,7 @@ Definition val_ref_update :=
Let 'y := 'f 'x in
val_set 'p 'y.
Lemma rule_ref_update : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop),
Lemma rule_ref_update : forall (f:val) (p:loc) (v:val) (H:hprop) (Q:val->hprop),
Normal_post Q -> (* todo: this might not be needed if using "normally" *)
(triple (f v)
PRE (RO(p ~~~> v) \* H)
......@@ -184,10 +184,10 @@ Proof using.
{ applys rule_get. }
{ intros x; simpl. xpull ;=> E. subst x.
applys rule_let' \[]. { hsimpl. }
applys~ rule_frame_read_only_conseq (p ~~~> v).
{ applys rule_consequence M; hsimpl. }
applys~ rule_frame_read_only_conseq (p ~~~> v).
{ applys rule_consequence M; hsimpl. }
{ hsimpl. }
{ clear M. intros y; simpl. xpull.
{ clear M. intros y; simpl. xpull.
applys~ rule_frame_conseq (Q y).
{ applys rule_set. }
{ hsimpl~. } } }
......@@ -217,7 +217,7 @@ Qed.
Definition Box (n:int) (p:loc) :=
Definition Box (n:int) (p:loc) :=
Hexists (q:loc), (p ~~~> q) \* (q ~~~> n).
Lemma Box_unfold : forall p n,
......@@ -248,7 +248,7 @@ Definition val_box_get :=
val_get 'q.
Lemma rule_box_get : forall p n,
triple (val_box_get p)
triple (val_box_get p)
PRE (RO (p ~> Box n))
POST (fun r => \[r = val_int n]).
Proof using.
......@@ -262,38 +262,38 @@ Qed.
(*---*)
(* let box_twice f p =
let q = !p in
q := f !q + f !q
(* let box_twice f p =
let q = !p in
q := f !q + f !q
*)
Definition val_box_twice :=
ValFun 'f 'p :=
Let 'q := val_get 'p in
Let 'n1 := val_get 'q in
Let 'n1 := val_get 'q in
Let 'a1 := 'f 'n1 in
Let 'n2 := val_get 'q in
Let 'n2 := val_get 'q in
Let 'a2 := 'f 'n2 in
Let 'm := 'a1 '+ 'a2 in
val_set 'q 'm.
Lemma rule_box_twice : forall (f:val) p n (F:int->int),
(forall (x:int) H, triple (val_box_twice f x)
(forall (x:int) H, triple (val_box_twice f x)
PRE (RO(p ~> Box n) \* H)
POST (fun r => \[r = val_int (F x)] \* H)) ->
triple (val_box_twice f p)
triple (val_box_twice f p)
PRE (p ~> Box n)
POST (fun r => \[r = val_unit] \* p ~> Box (2 * F n)).
Proof using.
introv M. xdef. xchange (Box_unfold p). xpull ;=> q.
applys rule_let' __ (p ~~~> q).
applys rule_let' __ (p ~~~> q).
{ hsimpl. }
{ rew_heap. applys rule_get. }
{ rew_heap. applys rule_get. }
{ intros x; simpl; xpull ;=> E; subst x.
applys rule_let' __ (q ~~~> n).
applys rule_let' __ (q ~~~> n).
{ hsimpl. }
{ rew_heap. applys rule_get. }
{ intros x; simpl; xpull ;=> E; subst x.
{ rew_heap. applys rule_get. }
{ intros x; simpl; xpull ;=> E; subst x.
Abort.
......
......@@ -308,7 +308,7 @@ Implicit Types f x : var.
Lemma triple_apps_funs_of_cf_iter : forall n F (vs:vals) xs t H Q,
F = val_funs xs t ->
var_funs_exec (length vs) xs ->
func_iter n cf_def cf (substs xs vs t) H Q ->
func_iter n cf_def cf (substn xs vs t) H Q ->
triple (trm_apps F vs) H Q.
Proof using.
introv EF N M. rewrite var_funs_exec_eq in N. rew_istrue in N.
......@@ -318,7 +318,7 @@ Qed.
Lemma triple_apps_fixs_of_cf_iter : forall n f F (vs:vals) xs t H Q,
F = val_fixs f xs t ->
var_fixs_exec f (length vs) xs ->
func_iter n cf_def cf (subst f F (substs xs vs t)) H Q ->
func_iter n cf_def cf (subst f F (substn xs vs t)) H Q ->
triple (trm_apps F vs) H Q.
Proof using.
introv EF N M. rewrite var_fixs_exec_eq in N. rew_istrue in N.
......
......@@ -344,7 +344,7 @@ Lemma Triple_apps_funs_of_Cf_iter : forall n F (Vs:dyns) (vs:vals) xs t A `{EA:E
F = val_funs xs t ->
vs = encs Vs ->
var_funs_exec (length Vs) xs ->
func_iter n Cf_def Cf (Substs xs Vs t) A EA H Q ->
func_iter n Cf_def Cf (Substn xs Vs t) A EA H Q ->
Triple (trm_apps F vs) H Q.
Proof using.
introv EF EV N M. rewrite var_funs_exec_eq in N. rew_istrue in N.
......@@ -355,7 +355,7 @@ Lemma Triple_apps_fixs_of_Cf_iter : forall n F f (Vs:dyns) (vs:vals) xs t A `{EA
F = val_fixs f xs t ->
vs = encs Vs ->
var_fixs_exec f (length Vs) xs ->
func_iter n Cf_def Cf (subst f F (Substs xs Vs t)) A EA H Q ->
func_iter n Cf_def Cf (subst f F (Substn xs Vs t)) A EA H Q ->
Triple (trm_apps (val_fixs f xs t) vs) H Q.
Proof using.
introv EF EV N M. rewrite var_fixs_exec_eq in N. rew_istrue in N.
......
(**
This file formalizes characteristic formulae for
This file formalizes characteristic formulae for
Separation Logic with read-only permissions.
Author: Arthur Charguéraud.
......@@ -25,10 +25,10 @@ Import TripleLowLevel. (* TODO: remove *)
Lemma on_rw_sub_union : forall (H1 H2:hprop) h1 h2,
on_rw_sub H1 h1 ->
H2 h2 ->
normal H2 ->
normal H2 ->
heap_compat h1 h2 ->
on_rw_sub (H1 \* H2) (h1 \u h2).
Proof using.
Proof using.
(*
introv (h11&h12&N1&N2&N3&N4) M2 C. hnf.
subst h1. lets~ (N1a&N1b): heap_compat_union_l_inv C.
......@@ -55,7 +55,7 @@ Proof using.
skip Dd: (heap_compat h11' h2).
skip De: (heap_compat h11' h12). (* TODO URGENT *)
exists (h11' \u h12) v. splits.
{ auto. }
{ auto. }
{ subst h1. do 2 rewrite~ heap_union_assoc. }
{ subst. do 2 rewrite~ heap_union_r. rewrite~ T3. }
{ applys on_rw_sub_htop. applys on_rw_sub_weaken R3.
......@@ -374,7 +374,7 @@ Implicit Types f x : var.
Lemma triple_apps_funs_of_cf_iter : forall n F (vs:vals) xs t H Q,
F = val_funs xs t ->
var_funs_exec (length vs) xs ->
func_iter n cf_def cf (substs xs vs t) H Q ->
func_iter n cf_def cf (substn xs vs t) H Q ->
triple (trm_apps F vs) H Q.
Proof using.
introv EF N M. rewrite var_funs_exec_eq in N. rew_istrue in N.
......@@ -384,7 +384,7 @@ Qed.
Lemma triple_apps_fixs_of_cf_iter : forall n f F (vs:vals) xs t H Q,
F = val_fixs f xs t ->
var_fixs_exec f (length vs) xs ->
func_iter n cf_def cf (subst f F (substs xs vs t)) H Q ->
func_iter n cf_def cf (subst f F (substn xs vs t)) H Q ->
triple (trm_apps F vs) H Q.
Proof using.
introv EF N M. rewrite var_fixs_exec_eq in N. rew_istrue in N.
......
......@@ -3850,8 +3850,8 @@ Fixpoint ctx_subst (E:ctx) (t:trm) : trm :=
| trm_val v => trm_val v
| trm_var x => match ctx_lookup x E with
| None => t
| Some v => trm_val v
end
| Some v => trm_val v
end
| trm_fun x t1 => trm_fun x (aux_no_capture x t1)
| trm_fix f x t1 => trm_fix f x (if eq_var_dec f y then t1 else
aux_no_capture x t1)
......@@ -3929,9 +3929,270 @@ Lemma ctx_subst_add_rem : forall E x v t,
= ctx_subst (ctx_add x v E) t.
Proof using.
intros E. induction E as [|(y,w) E']; intros.
{ auto. }
{ auto. }
{ simpl ctx_rem. unfold ctx_add. case_if.
{ subst y. admit. }
{ simpls. rewrite subst_subst_cross; [|auto]. apply IHE'. } }
Qed.
*)
Fixpoint substn (xs:vars) (vs:vals) (t:trm) : trm :=
match xs, vs with
| x::xs', v::vs' => substn xs' vs' (subst x v t)
| _, _ => t
end.
Lemma substs_eq_substs : forall xs vs t,
length xs = length vs ->
substs xs vs t = substn (LibList.combine xs vs) t.
Proof using.
intros xs. induction xs as [|x xs']; introv N;
destruct vs as [|v vs']; rew_list in N; tryfalse.
{ auto. }
{ simpl. rewrite~ IHxs'. }
Qed.
Lemma subst_substn : forall x v ys ws t,
var_fresh x ys ->
length ys = length ws ->
subst x v (substn ys ws t) = substn ys ws (subst x v t).
Proof using.
intros. gen t ws. induction ys as [|y ys']; introv L. simpls.
{ auto. }
{ destruct ws as [|w ws']; rew_list in *. { false; math. }
simpls. case_if. rewrite~ IHys'. fequals. rewrite~ subst_subst_cross. }
Qed.
==now==
(* ===================
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xseq] *)
Ltac xseq_core tt ::=
applys local_erase; esplit; split.
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xlet] *)
Ltac xlet_core tt ::=
applys local_erase; esplit; split.
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xif] *)
Ltac xif_core tt ::=
applys local_erase; esplit; splits;
[ try reflexivity
| xif_post tt
| xif_post tt ].
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xfail] *)
Ltac xfail_core tt ::=
applys local_erase; unfold wp_fail.
(* ---------------------------------------------------------------------- *)
(* * [xapp] and [xapps] and [xapp as] *)
(** Basic [xapp] implementation
Tactic Notation "xapp" constr(E) :=
applys local_erase; xapplys E.
Tactic Notation "xapp" :=
try applys local_erase;
xspec;
let H := fresh "TEMP" in intros H;
xapplys H;
clear H.
*)
Ltac hpull_cont tt ::=
try hpull.
Ltac hsimpl_cont tt ::=
hsimpl.
Ltac xapp_let_cont tt ::=
let X := fresh "X" in intros X;
instantiate; try xpull; gen X.
Ltac xapp_as_let_cont tt ::=
instantiate; try xpull.
Ltac xapps_let_cont tt ::=
let X := fresh "X" in intros X;
instantiate; try xpull;
first [ intro_subst | gen X ].
Ltac xapp_template xlet_tactic xapp_tactic xlet_cont ::=
match goal with
| |- local (wp_let _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
| |- local (wp_if _ _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
| |- local (wp_seq _ _) _ _ => xseq; [ xapp_tactic tt | ]
| _ => xapp_tactic tt
end.
Ltac xapp_xapply E cont_post :=
match goal with
| |- ?F ?H ?Q => is_evar Q; xapplys E
| |- ?F ?H (fun r => \[r = val_unit] \* ?H') => is_evar H'; xapplys E
(* TODO: might not be needed *)
| _ => xapply_core E ltac:(fun tt => hcancel) ltac:(cont_post)
end.
Ltac xapp_basic_prepare tt ::=
try match goal with |- local _ _ _ => apply local_erase end;
rew_nary.
Ltac xapp_with_args E cont_xapply ::=
match E with
| __ => (* no spec provided *)
let S := fresh "Spec" in
xspec;
intros S;
cont_xapply S;
clear S
| _ =>
match list_boxer_of E with
| cons (boxer ltac_wild) ?E' => (* only args provided *)
let S := fresh "Spec" in
xspec;
intros S;
cont_xapply ((boxer S)::E');
clear S
| _ => (* spec and args provided *)
cont_xapply E
end
end.
Ltac xapp_basic E cont_post tt ::=
xapp_basic_prepare tt;
xapp_with_args E ltac:(fun H =>
xapp_xapply H cont_post).
(* TODO: xapps should do hsimpl if not in a let *)
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xval] and [xvals] *)
Ltac xval_nohtop_core tt :=
applys local_erase; unfold wp_val.
Tactic Notation "xval_nohtop" :=
xval_nohtop_core tt.
Lemma xval_htop_lemma : forall v H Q,
H ==> Q v \* \Top ->
local (wp_val v) H Q.
Proof using.
intros v H Q M. unfold wp_val.
applys~ local_htop_post (Q \*+ \Top).
applys local_erase. intros x.
hpull. intro_subst. hchanges~ M.
Qed.
Lemma xval_htop_as_lemma : forall v H Q,
(forall x, x = v -> H ==> Q x \* \Top) ->
local (wp_val v) H Q.
Proof using. intros v H Q M. applys~ xval_htop_lemma. Qed.
Ltac xval_template xlet_tactic xval_tactic xlet_cont :=
match goal with
| |- local (wp_let _ _) _ _ => xlet_tactic tt; [ xval_tactic tt | xlet_cont tt ]
| |- local (wp_if _ _ _) _ _ => xlet_tactic tt; [ xval_tactic tt | xlet_cont tt ]
| _ => xval_tactic tt
end.
Ltac xval_basic tt :=
match goal with
| |- local ?F ?H ?Q => is_evar Q; applys local_erase; applys refl_rel_incl'
| _ => applys xval_htop_lemma
end.
Ltac xval_as_basic X EX :=
match goal with
| |- local ?F ?H ?Q => is_evar Q; applys local_erase; applys refl_rel_incl'
| _ => applys xval_htop_as_lemma; intros X EX
end.
Ltac xval_core tt ::=
xval_template ltac:(fun tt => xlet) ltac:(xval_basic) ltac:(xapp_let_cont).
Ltac xval_as_core X ::=
match goal with
| |- local (wp_val _) _ _ => let EX := fresh "E" X in xval_as_basic X EX
| _ => xval_template ltac:(fun tt => xlet as X) ltac:(xval_basic) ltac:(xapp_as_let_cont)
end.
Ltac xvals_core tt ::=
match goal with
| |- local (wp_val _) _ _ => xval_basic tt; hsimpl
| _ => xval_template ltac:(fun tt => xlet) ltac:(xval_basic) ltac:(xapps_let_cont)
end.
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xwhile] *)
(*
Ltac xwhile_template xwhile_tactic xseq_cont :=
match goal with
| |- local (wp_seq _ _) _ _ => xseq; [ xwhile_tactic tt | xseq_cont tt ]
| _ => xwhile_tactic tt
end.
Ltac xwhile_intros_all R LR HR ::=
intros R LR; hnf; intros HR.
Ltac xwhile_intros R ::=
let LR := fresh "L" R in
let HR := fresh "H" R in
xwhile_intros_all R LR HR.
Ltac xwhile_basic xwhile_intros_tactic ::=
applys local_erase;
xwhile_intros_tactic tt.
Ltac xwhile_core xwhile_tactic ::=
xwhile_template ltac:(xwhile_tactic) ltac:(fun tt => xpull).
*)
*)
\ No newline at end of file
This diff is collapsed.
......@@ -624,7 +624,7 @@ Qed.
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
F = (val_funs xs t1) ->
var_funs (length Vs) xs ->
triple (substs xs Vs t1) H Q ->
triple (substn xs Vs t1) H Q ->
triple (trm_apps F Vs) H Q.
Proof using.
introv E N M. intros H' h Hf. forwards (h'&v&R&K): (rm M) Hf.
......@@ -634,7 +634,7 @@ Qed.
Lemma rule_apps_fixs : forall xs f F (Vs:vals) t1 H Q,
F = (val_fixs f xs t1) ->
var_fixs f (length Vs) xs ->
triple (subst f F (substs xs Vs t1)) H Q ->
triple (subst f F (substn xs Vs t1)) H Q ->
triple (trm_apps F Vs) H Q.
Proof using.
introv E N M. intros H' h Hf. forwards (h'&v&R&K): (rm M) Hf.
......@@ -1085,7 +1085,7 @@ Qed.
Definition spec_funs (xs:vars) (t1:trm) (F:val) :=
forall (Xs:vals), length xs = length Xs ->
triple (substs xs Xs t1) ===> triple (trm_apps F Xs).
triple (substn xs Xs t1) ===> triple (trm_apps F Xs).
Lemma spec_funs_val_funs : forall xs t1,
var_distinct xs ->
......@@ -1099,7 +1099,7 @@ Proof using. introv D N L M. applys* rule_apps_funs. splits~. Qed.
Definition spec_fixs (f:var) (xs:vars) (t1:trm) (F:val) :=
forall (Xs:vals), length xs = length Xs ->
triple (subst f F (substs xs Xs t1)) ===> triple (trm_apps F Xs).
triple (subst f F (substn xs Xs t1)) ===> triple (trm_apps F Xs).
Lemma spec_fixs_val_fixs : forall f xs t1,
var_distinct (f::xs) ->
......
......@@ -410,8 +410,8 @@ Arguments Hfield_not_null : clear implicits.
Definition Subst (y:var) (d:dyn) (t:trm) : trm :=
subst y (enc d) t.
Definition Substs (ys:vars) (ds:dyns) (t:trm) : trm :=
substs ys (encs ds) t.
Definition Substn (ys:vars) (ds:dyns) (t:trm) : trm :=
substn ys (encs ds) t.
(* ********************************************************************** *)
......@@ -592,7 +592,7 @@ Qed.
Lemma Rule_apps_funs : forall xs F (Vs:dyns) t1 H A `{EA: Enc A} (Q:A->hprop),
F = (val_funs xs t1) ->
var_funs (length Vs) xs ->
Triple (Substs xs Vs t1) H Q ->
Triple (Substn xs Vs t1) H Q ->
Triple (trm_apps F (encs Vs)) H Q.
Proof using.
introv E N M. unfold Triple. applys* rule_apps_funs. rewrite~ length_encs.
......@@ -601,7 +601,7 @@ Qed.
Lemma Rule_apps_fixs : forall xs f F (Vs:dyns) t1 H A `{EA: Enc A} (Q:A->hprop),
F = (val_fixs f xs t1) ->
var_fixs f (length Vs) xs ->
Triple (subst f F (Substs xs Vs t1)) H Q ->
Triple (subst f F (Substn xs Vs t1)) H Q ->
Triple (trm_apps F (encs Vs)) H Q.
Proof using.
introv E N M. unfold Triple. applys* rule_apps_fixs. rewrite~ length_encs.
......@@ -740,7 +740,7 @@ Proof using. intros. unfold Triple, Post. xapplys~ rule_ptr_add_nat. Qed.
Definition Spec_funs (xs:vars) (t1:trm) (F:val) :=
forall (Xs:dyns), length xs = length Xs ->
Triple (Substs xs Xs t1) ===> Triple (trm_apps F (encs Xs)).
Triple (Substn xs Xs t1) ===> Triple (trm_apps F (encs Xs)).
Lemma spec_funs_val_funs : forall xs t1,
var_distinct xs ->
......@@ -754,7 +754,7 @@ Proof using. introv D N E M. applys* Rule_apps_funs. splits~. Qed.
Definition Spec_fixs (f:var) (xs:vars) (t1:trm) (F:val) :=
forall (Xs:dyns), length xs = length Xs ->
Triple (subst f F (Substs xs Xs t1)) ===> Triple (trm_apps F (encs Xs)).
Triple (subst f F (Substn xs Xs t1)) ===> Triple (trm_apps F (encs Xs)).
Lemma Spec_fixs_val_fixs : forall f xs t1,
var_distinct (f::xs) ->
......
......@@ -1647,7 +1647,7 @@ Qed.
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
F = (val_funs xs t1) ->
var_funs (LibList.length Vs) xs ->
triple (substs xs Vs t1) H Q ->
triple (substn xs Vs t1) H Q ->
triple (trm_apps F Vs) H Q.
Proof using.
introv E N M. intros h1 h2 D H1.
......
......@@ -18,6 +18,35 @@ Generalizable Variables A.
Ltac auto_star ::= jauto.
(* TODO: move to TLC buffer *)
Lemma list2_ind : forall A B (P:list A->list B->Prop) l1 l2,
length l1 = length l2 ->
P nil nil ->
(forall x1 xs1 x2 xs2, P xs1 xs2 -> P (x1::xs1) (x2::xs2)) ->
P l1 l2.
Proof using.
introv E M1 M2. gen l2. induction l1 as [|x1 l1']; intros;
destruct l2 as [|x2 l2']; try solve [false; math]; auto.
Qed.
Tactic Notation "list2_ind" constr(l1) constr(l2) :=
pattern l2; pattern l1;
match goal with |- (fun a => (fun b => @?P a b) _) _ =>
(* applys list2_ind P *)
let X := fresh "P" in set (X := P); applys list2_ind X; unfold X; try clear X
end.
Tactic Notation "list2_ind" "~" constr(l1) constr(l2) :=
list2_ind l1 l2; auto_tilde.
Tactic Notation "list2_ind" "*" constr(l1) constr(l2) :=
list2_ind l1 l2; auto_star.
Tactic Notation "list2_ind" constr(E) :=
match type of E with length ?l1 = length ?l2 =>
list2_ind l1 l2; [ apply E | | ] end.
(* ********************************************************************** *)
(* * Derived basic functions, useful for metaprogramming *)
......@@ -33,63 +62,61 @@ Proof using. auto. Qed.