From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 15 Nov 2008 13:18:05 +0000 (+0000)
Subject: housekeeping
X-Git-Tag: make_still_working~4559
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9762655f6853bacf4786dab274afa4c33d3e32f3;hp=f1f445457c73202fd696c1b9fe0b24c0bafe2452;p=helm.git

housekeeping
---

diff --git a/helm/software/matita/contribs/didactic/algebra.ma b/helm/software/matita/contribs/didactic/algebra.ma
deleted file mode 100644
index 17c30e341..000000000
--- a/helm/software/matita/contribs/didactic/algebra.ma
+++ /dev/null
@@ -1,101 +0,0 @@
-
-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.
diff --git a/helm/software/matita/contribs/didactic/depends b/helm/software/matita/contribs/didactic/depends
deleted file mode 100644
index ae4b2462a..000000000
--- a/helm/software/matita/contribs/didactic/depends
+++ /dev/null
@@ -1,9 +0,0 @@
-duality.ma nat/minus.ma
-exercise-induction.ma nat/minus.ma
-shannon.ma nat/minus.ma
-algebra.ma nat/compare.ma nat/times.ma
-exercise-duality.ma nat/minus.ma
-induction.ma nat/minus.ma
-nat/compare.ma 
-nat/minus.ma 
-nat/times.ma 
diff --git a/helm/software/matita/contribs/didactic/depends.png b/helm/software/matita/contribs/didactic/depends.png
deleted file mode 100644
index ed54ff73b..000000000
Binary files a/helm/software/matita/contribs/didactic/depends.png and /dev/null differ
diff --git a/helm/software/matita/contribs/didactic/root b/helm/software/matita/contribs/didactic/root
deleted file mode 100644
index 8f72072f4..000000000
--- a/helm/software/matita/contribs/didactic/root
+++ /dev/null
@@ -1 +0,0 @@
-baseuri=cic:/matita/didactic