+++ /dev/null
-
-include "nat/times.ma".
-include "nat/compare.ma".
-
-definition if_then_else ≝ λT:Type.λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
-notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 90 for @{ 'if_then_else $e $t $f }.
-notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 90 for @{ 'if_then_else $e $t $f }.
-interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
-
-inductive F : Type ≝
-| EZero : F
-| EOne : F
-| EPlus : F → F → F
-| ETimes : F → F → F
-| X : ℕ → F
-.
-
-let rec val (E : F) (v : ℕ → ℕ) on E : ℕ :=
- match E with
- [ X i ⇒ v i
- | EPlus e1 e2 ⇒ (val e1 v) + (val e2 v)
- | ETimes e1 e2 ⇒ (val e1 v) * (val e2 v)
- | EZero ⇒ 0
- | EOne ⇒ 1
- ]
- .
-
-definition v201 ≝ λx.
- if (eqb x 0) then 2
- else if (eqb x 1) then 0
- else if (eqb x 2) then 1
- else 0
-.
-
-eval normalize on
- (val
- (EPlus (X 3)
- (ETimes EOne (X 2))) v201).
-
-let rec subst (E : F) (G : F) (i : ℕ) on E : F :=
- match E with
- [ X j => if (eqb i j) then G else (X j)
- | EPlus e1 e2 => EPlus (subst e1 G i) (subst e2 G i)
- | ETimes e1 e2 => ETimes (subst e1 G i) (subst e2 G i)
- | EZero => EZero
- | EOne => EOne
- ]
- .
-
-eval normalize on
- (subst
- (EPlus (X 0) (ETimes (X 1) (X 2)))
- (EOne)
- 1)
- .
-
-definition equiv :=
- λe1,e2.∀v. val e1 v = val e2 v.
-
-theorem sostituzione :
- ∀E1,E2,G,i.
- equiv E1 E2 → equiv (subst G E1 i) (subst G E2 i).
-assume E1 : F.
-assume E2 : F.
-assume G : F.
-assume i : ℕ.
-suppose (equiv E1 E2) (H).
-we proceed by induction on G to prove
- (equiv (subst G E1 i) (subst G 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
- (∀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.
projects / helm.git / commitdiff
