From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 20 Jul 2009 19:36:04 +0000 (+0000)
Subject: nrewrite now working
X-Git-Tag: make_still_working~3647
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=efd42476895cfb9b7048cc81848cd1c60f394367;p=helm.git

nrewrite now working
---

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 4fac05b51..40400378d 100644
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -73,20 +73,17 @@ ndefinition sub_magma ≝
 ndefinition image: ∀A,B. (A → B) → Ω \sup A → Ω \sup B ≝
  λA,B,f,Sa. {y | ∃x. x ∈ Sa ∧ f x = y}.
 
-naxiom daemon: False.
-
 ndefinition mm_image:
  ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma B.
  #A; #B; #Ma; #Mb; #f;
  napply (mk_magma ???)
-  [ napply (image ?? (mmcarr ?? (mmmcarr ???? f)) Ma) (* NO COMPOSITE! *)
+  [ napply (image ?? f Ma)
   | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
     napply (ex_intro ????)
      [ napply (op ? x0 y0) 
      | napply (conj ????)
         [ napply (op_closed ??????); nassumption
-        | (* nrewrite < Hx1; DOES NOT WORK *)
-          napply (eq_rect ?? (λ_.?) ?? Hx1);
-          napply (eq_rect ?? (λ_.?) ?? Hy1);
+        | nrewrite < Hx1;
+          nrewrite < Hy1;
           napply (mmprop ?? f ??)]##]
 nqed.
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index 2aca2bbd3..379c57656 100644
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -1,7 +1,6 @@
 sets/sets.ma logic/equality.ma
 topology/igt.ma logic/connectives.ma properties/relations.ma
 logic/equality.ma logic/connectives.ma
-.unnamed.ma logic/pts.ma
 logic/connectives.ma logic/pts.ma
 algebra/magmas.ma sets/sets.ma
 properties/relations.ma logic/pts.ma
diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot
index 8898c6c2e..9069f0cd9 100644
--- a/helm/software/matita/nlibrary/depends.dot
+++ b/helm/software/matita/nlibrary/depends.dot
@@ -6,8 +6,6 @@ digraph g {
   "topology/igt.ma" -> "properties/relations.ma" [];
   "logic/equality.ma" [];
   "logic/equality.ma" -> "logic/connectives.ma" [];
-  ".unnamed.ma" [];
-  ".unnamed.ma" -> "logic/pts.ma" [];
   "logic/connectives.ma" [];
   "logic/connectives.ma" -> "logic/pts.ma" [];
   "algebra/magmas.ma" [];
diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png
index 6d8cfcfd9..c00871d4a 100644
Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ
diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
index 2418f2a7c..1da7e1b0b 100644
--- a/helm/software/matita/nlibrary/logic/equality.ma
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -17,11 +17,6 @@ include "logic/connectives.ma".
 ninductive eq (A: Type) (a: A) : A → CProp ≝
  refl: eq A a a.
 
-nlet rec eq_rect (A: Type) (x: A) (P: ∀y:A. eq A x y → CProp) (q: P x (refl A x))
- (y: A) (p: eq A x y) on p : P y p ≝
- match p with
-  [ refl ⇒ q ].
- 
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).