From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 13 Jul 2009 09:13:12 +0000 (+0000)
Subject: First proof finished (some tactics still not working).
X-Git-Tag: make_still_working~3691
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6003ba0e4600778c6055ed5ea5cb6c1fba3abe32;p=helm.git

First proof finished (some tactics still not working).
---

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 7283cbc58..4fac05b51 100644
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -47,6 +47,10 @@ ndefinition mmcarr ≝
  λA,B.λf: pre_magma_morphism A B. match f with [ mk_pre_magma_morphism f _ ⇒ f ].
 ncoercion mmcarr: ∀A,B.∀M: pre_magma_morphism A B. A → B ≝ mmcarr
  on _M: pre_magma_morphism ? ? to ∀_.?.
+ndefinition mmprop ≝
+ λA,B,M.
+  match M return λM:pre_magma_morphism A B.∀x,y. M (op ? x y) = op ? (M x) (M y) with
+   [ mk_pre_magma_morphism _ p ⇒ p ].
 
 nrecord magma_morphism (A) (B) (Ma: magma A) (Mb: magma B) : Type ≝
  { mmmcarr: pre_magma_morphism A B;
@@ -81,5 +85,8 @@ ndefinition mm_image:
      [ napply (op ? x0 y0) 
      | napply (conj ????)
         [ napply (op_closed ??????); nassumption
-        | nelim daemon ]##]
+        | (* nrewrite < Hx1; DOES NOT WORK *)
+          napply (eq_rect ?? (λ_.?) ?? Hx1);
+          napply (eq_rect ?? (λ_.?) ?? Hy1);
+          napply (mmprop ?? f ??)]##]
 nqed.
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
index ff8cc5a13..2418f2a7c 100644
--- a/helm/software/matita/nlibrary/logic/equality.ma
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -16,6 +16,11 @@ 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).