From 4d4ea7cf3ab9ca05fa41c3f7b680cb10232acb82 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 20 Oct 2008 13:47:30 +0000
Subject: [PATCH] ...

---
 .../matita/contribs/didactic/algebra.ma       | 84 +++++++++++++++++++
 1 file changed, 84 insertions(+)
 create mode 100644 helm/software/matita/contribs/didactic/algebra.ma

diff --git a/helm/software/matita/contribs/didactic/algebra.ma b/helm/software/matita/contribs/didactic/algebra.ma
new file mode 100644
index 000000000..eabbdb110
--- /dev/null
+++ b/helm/software/matita/contribs/didactic/algebra.ma
@@ -0,0 +1,84 @@
+
+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 ≝
+| X       : ℕ → F
+| EPlus   : F → F → F
+| ETimes  : F → F → F
+| EZero   : F
+| EOne    : 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 X.
+  assume n : ℕ.
+  the thesis becomes 
+    (equiv 
+      (if (eqb i n) then E1 else (X n))
+      (subst (X n) E2 i)).
+  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
-- 
2.39.2