Commit 5e795ba1 by MARCHE Claude

### WP: finished proof of eval_subst

parent 2d864119
 ... @@ -135,7 +135,7 @@ function subst (f:fmla) (x:ident) (v:ident) : fmla = ... @@ -135,7 +135,7 @@ function subst (f:fmla) (x:ident) (v:ident) : fmla = | Fand f1 f2 -> Fand (subst f1 x v) (subst f2 x v) | Fand f1 f2 -> Fand (subst f1 x v) (subst f2 x v) | Fnot f -> Fnot (subst f x v) | Fnot f -> Fnot (subst f x v) | Fimplies f1 f2 -> Fimplies (subst f1 x v) (subst f2 x v) | Fimplies f1 f2 -> Fimplies (subst f1 x v) (subst f2 x v) | Flet y t f -> Flet y t (subst f x v) | Flet y t f -> Flet y (subst_term t x v) (subst f x v) | Fforall y ty f -> Fforall y ty (subst f x v) | Fforall y ty f -> Fforall y ty (subst f x v) end end ... ...
This diff is collapsed.
 ... @@ -172,7 +172,7 @@ Fixpoint subst(f:fmla) (x:Z) (v:Z) {struct f}: fmla := ... @@ -172,7 +172,7 @@ Fixpoint subst(f:fmla) (x:Z) (v:Z) {struct f}: fmla := | (Fand f1 f2) => (Fand (subst f1 x v) (subst f2 x v)) | (Fand f1 f2) => (Fand (subst f1 x v) (subst f2 x v)) | (Fnot f1) => (Fnot (subst f1 x v)) | (Fnot f1) => (Fnot (subst f1 x v)) | (Fimplies f1 f2) => (Fimplies (subst f1 x v) (subst f2 x v)) | (Fimplies f1 f2) => (Fimplies (subst f1 x v) (subst f2 x v)) | (Flet y t f1) => (Flet y t (subst f1 x v)) | (Flet y t f1) => (Flet y (subst_term t x v) (subst f1 x v)) | (Fforall y ty f1) => (Fforall y ty (subst f1 x v)) | (Fforall y ty f1) => (Fforall y ty (subst f1 x v)) end. end. Unset Implicit Arguments. Unset Implicit Arguments. ... @@ -199,6 +199,24 @@ rewrite IHf2; tauto. ... @@ -199,6 +199,24 @@ rewrite IHf2; tauto. simpl; intros (F1&F2&F3). simpl; intros (F1&F2&F3). rewrite IHf; auto. rewrite IHf; auto. rewrite Select_neq; auto. rewrite Select_neq; auto. rewrite eval_subst_term; tauto. simpl; intros (F1&F2). destruct d; simpl. split; intros. generalize (H n). intro h. rewrite IHf in h; auto. rewrite Select_neq in h; auto. rewrite IHf; auto. rewrite Select_neq; auto. split; intros. generalize (H b). intro h. rewrite IHf in h; auto. rewrite Select_neq in h; auto. rewrite IHf; auto. rewrite Select_neq; auto. Qed. Qed. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!