First proof finished (some tactics still not working).

[helm.git] / helm / software / matita / nlibrary / algebra / magmas.ma

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index e49d8ea82545549e7b9c3818f1ba029879ede330..4fac05b51c6e2926fdaa85f21e9edc8db03561a0 100644 (file)
--- 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;
@@ -58,10 +62,6 @@ ndefinition mmmcarr ≝
 ncoercion mmmcarr : ∀A,B,Ma,Mb.∀f: magma_morphism A B Ma Mb. pre_magma_morphism A B
  ≝ mmmcarr
  on _f: magma_morphism ???? to pre_magma_morphism ??.
-ndefinition mmcarr_mmmcarr ≝
- λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb. mmcarr ?? (mmmcarr ???? f).
-ncoercion mmcarr_mmmcarr : ∀A,B,Ma,Mb.∀f: magma_morphism A B Ma Mb. A → B ≝ mmcarr_mmmcarr
- on _f: magma_morphism ???? to ∀_.?.
 ndefinition mmclosed ≝
  λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb.
   match f return λf: magma_morphism A B Ma Mb.∀x. x ∈ Ma → f x ∈ Mb with
@@ -79,11 +79,14 @@ 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)) (mcarr ? Ma)) 
+  [ napply (image ?? (mmcarr ?? (mmmcarr ???? f)) Ma) (* NO COMPOSITE! *)
   | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
     napply (ex_intro ????)
      [ 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