proposition: Lemma subInterpFormula : forall (value : nat -> U M) (f : Formula L) (v : nat) (s : Term L), interpFormula (updateValue value v (interpTerm value s)) f <-> interpFormula value (substF f v s).
proof: Proof. intros value f; revert value. elim f using Formula_depth_ind2; simpl. - intros t t0 value v s; repeat rewrite subInterpTerm. tauto. - intros r t value v s; apply subInterpRel. - intros f0 H f1 H0 value v s; rewrite (subFormulaImp L). simpl; assert (H1: interpFormula (updateValue value v (interpTerm value s)) f1 <-> interpFormula value (substF f1 v s)) by auto. assert (H2: interpFormula (updateValue value v (interpTerm value s)) f0 <-> interpFormula value (substF f0 v s)) by auto. tauto. - intros f0 H value v s; rewrite (subFormulaNot L). simpl in |- *. assert (interpFormula (updateValue value v (interpTerm value s)) f0 <-> interpFormula value (substF f0 v s)). auto. tauto. - intros v a H value v0 s; rewrite (subFormulaForall L). induction (eq_nat_dec v v0) as [a0 | b]. + rewrite a0. simpl in |- *. unfold updateValue in |- *. split. * intros H0 x; apply freeVarInterpFormula with (fun x0 : nat => match eq_nat_dec v0 x0 with | left _ => x | right _ => match eq_nat_dec v0 x0 with | left _ => interpTerm value s | right _ => value x0 end end). -- intros x0 H1; induction (eq_nat_dec v0 x0); reflexivity. -- auto. * intros H0 x; apply freeVarInterpFormula with (fun x0 : nat => match eq_nat_dec v0 x0 with | left _ => x | right _ => value x0 end). -- intros x0 H1; induction (eq_nat_dec v0 x0); reflexivity. -- auto. + induction (In_dec eq_nat_dec v (freeVarT s)) as [a0 | b0]. * simpl; set (nv := newVar (v0 :: freeVarT s ++ freeVarF a)) in *. assert (~ List.In nv (v0 :: freeVarT s ++ freeVarF a)). { unfold nv in |- *. apply newVar1. } assert (forall (x : U M) (x0 : nat), List.In x0 (freeVarF a) -> updateValue (updateValue value v0 (interpTerm value s)) v x x0 = updateValue (updateValue (updateValue value nv x) v0 (interpTerm (updateValue value nv x) s)) v (interpTerm (updateValue (updateValue value nv x) v0 (interpTerm (updateValue value nv x) s)) (var nv)) x0). { intros x x0 H1; unfold updateValue in |- *; simpl in |- *. induction (eq_nat_dec v x0) as [a1 | ?]. - induction (eq_nat_dec v0 nv) as [a2 | b0]. + elim H0. rewrite a2. simpl in |- *. auto. + induction (eq_nat_dec nv nv) as [a2 | b1]. * reflexivity. * elim b1; reflexivity. - induction (eq_nat_dec v0 x0) as [a1 | b1]. + apply freeVarInterpTerm. intros x1 H2; induction (eq_nat_dec nv x1). * elim H0. rewrite a2. simpl in |- *. auto with datatypes. * reflexivity. + induction (eq_nat_dec nv x0) as [a1 | ?]. * elim H0. rewrite a1. auto with datatypes. * reflexivity. } assert (H2: (forall x : U M, interpFormula (updateValue (updateValue (updateValue value nv x) v0 (interpTerm (updateValue value nv x) s)) v (interpTerm (updateValue (updateValue value nv x) v0 (interpTerm (updateValue value nv x) s)) (var nv))) a) <-> (forall x : U M, interpFormula (updateValue value nv x) (substF (substF a v (var nv)) v0 s))). { split. - assert (H2: forall b : Formula L, lt_depth L b (forallH v a) -> forall (value : nat -> U M) (v : nat) (s : Term L), interpFormula (updateValue value v (interpTerm value s)) b -> interpFormula value (substF b v s)). { intros b0 H2 value0 v1 s0 H3; induction (H b0 H2 value0 v1 s0); auto. } intros H3 x; apply H2. + eapply eqDepth. * symmetry; apply subFormulaDepth. * apply depthForall. + apply H2. * apply depthForall. * apply H3. - intros H2 x. assert (H3: forall b : Formula L, lt_depth L b (allH v, a)%fol -> forall (value : nat -> U M) (v : nat) (s : Term L), interpFormula value (substF b v s) -> interpFormula (updateValue value v (interpTerm value s)) b) by (intros; induction (H b0 H3 value0 v1 s0); auto). clear H; apply H3. + apply depthForall. + apply H3. * eapply eqDepth. -- symmetry; apply subFormulaDepth. -- apply depthForall. * auto. } assert (H3: (forall x : U M, interpFormula (updateValue (updateValue value v0 (interpTerm value s)) v x) a) <-> (forall x : U M, interpFormula (updateValue (updateValue (updateValue value nv x) v0 (interpTerm (updateValue value nv x) s)) v (interpTerm (updateValue (updateValue value nv x) v0 (interpTerm (updateValue value nv x) s)) (var nv))) a)). { split. - intros H3 x; apply freeVarInterpFormula with (updateValue (updateValue value v0 (interpTerm value s)) v x). auto. auto. - intros H3 x. apply freeVarInterpFormula with (updateValue (updateValue (updateValue value nv x) v0 (interpTerm (updateValue value nv x) s)) v (interpTerm (updateValue (updateValue value nv x) v0 (interpTerm (updateValue value nv x) s)) (var nv))). + intros x0 H4; symmetry in |- *. auto. + auto. } tauto. * simpl in |- *. assert (forall (x : U M) (x0 : nat), List.In x0 (freeVarF a) -> updateValue (updateValue value v0 (interpTerm value s)) v x x0 = updateValue (updateValue value v x) v0 (interpTerm (updateValue value v x) s) x0). { intros x x0 H0; unfold updateValue; induction (eq_nat_dec v x0) as [a0 | b1]. - induction (eq_nat_dec v0 x0) as [a1 | ?]. + elim b. transitivity x0; auto. + reflexivity. - induction (eq_nat_dec v0 x0) as [a0 | ?]. + apply freeVarInterpTerm. intros x1 H1; induction (eq_nat_dec v x1). * elim b0. rewrite a1. auto. * reflexivity. + reflexivity. } split. -- intros H1 x; assert (H2: forall b : Formula L, lt_depth L b (forallH v a) -> forall (value : nat -> U M) (v : nat) (s : Term L), interpFormula (updateValue value v (interpTerm value s)) b -> interpFormula value (substF b v s)). { intros b1 H2 value0 v1 s0 H3; induction (H b1 H2 value0 v1 s0); auto. } apply H2. ++ apply depthForall. ++ apply freeVarInterpFormula with (updateValue (updateValue value v0 (interpTerm value s)) v x). ** apply (H0 x). ** apply H1. -- assert (forall b : Formula L, lt_depth L b (forallH v a) -> forall (value : nat -> U M) (v : nat) (s : Term L), interpFormula value (substF b v s) -> interpFormula (updateValue value v (interpTerm value s)) b). { intros b1 H1 value0 v1 s0 H2; induction (H b1 H1 value0 v1 s0); auto. } intros H2 x; apply freeVarInterpFormula with (updateValue (updateValue value v x) v0 (interpTerm (updateValue value v x) s)). ++ intros; symmetry in |- *; auto. ++ apply H1. ** apply depthForall. ** auto. Qed.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)