interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
inductive F : Type ≝
-| X : ℕ → F
-| EPlus : F → F → F
-| ETimes : F → F → F
| EZero : F
| EOne : F
+| EPlus : F → F → F
+| ETimes : F → F → F
+| X : ℕ → F
.
let rec val (E : F) (v : ℕ → ℕ) on E : ℕ :=
suppose (equiv E1 E2) (H).
we proceed by induction on G to prove
(equiv (subst G E1 i) (subst G E2 i)).
-case X.
- assume n : ℕ.
- the thesis becomes
- (equiv
- (if (eqb i n) then E1 else (X n))
- (subst (X n) E2 i)).
+case EZero.
+ the thesis becomes (equiv (subst EZero E1 i) (subst EZero E2 i)).
+ the thesis becomes (equiv EZero (subst EZero E2 i)).
+ the thesis becomes (equiv EZero EZero).
+ the thesis becomes (∀v.val EZero v = val EZero v).
+ assume v : (ℕ → ℕ).
+ the thesis becomes (0 = val EZero v).
+ the thesis becomes (0 = 0).
+ done.
+case EOne.
+ the thesis becomes (∀v.val EOne v = val EOne v).
+ assume v : (ℕ → ℕ).
+ the thesis becomes (1 = 1).
+ done.
+case EPlus.
+ assume e1 : F.
+ by induction hypothesis we know (equiv (subst e1 E1 i) (subst e1 E2 i)) (H1).
+ assume e2 : F.
+ by induction hypothesis we know (equiv (subst e2 E1 i) (subst e2 E2 i)) (H2).
+ by H1 we proved (∀v.val (subst e1 E1 i) v = val (subst e1 E2 i) v) (H11).
+ by H2 we proved (∀v.val (subst e2 E1 i) v = val (subst e2 E2 i) v) (H22).
the thesis becomes
- (equiv
- (if (eqb i n) then E1 else (X n))
- (if (eqb i n) then E2 else (X n))).
- we proceed by cases ...
-
-
-
-
\ No newline at end of file
+ (∀v. val (subst e1 E1 i) v + val (subst e2 E1 i) v =
+ val (subst e1 E2 i) v + val (subst e2 E2 i) v).
+ assume v : (ℕ → ℕ).
+ conclude
+ (val (subst e1 E1 i) v + val (subst e2 E1 i) v) =
+ (val (subst e1 E1 i) v + val (subst e2 E2 i) v) by H11.
+ conclude
+ (val (subst e1 E1 i) v + val (subst e2 E1 i) v) =
+ (val (subst e1 E1 i) v + val (subst e2 E1 i) v) by H22.
+ done.