From 83d2e9c93f39464715e10fab6ebdb4be97c37b08 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 26 Oct 2010 13:09:00 +0000
Subject: [PATCH] Some files ported to intermediate syntax to test.

---
 matita/matita/nlibrary/logic/connectives.ma   |  20 +--
 matita/matita/nlibrary/logic/equality.ma      | 114 +++++++++---------
 .../matita/nlibrary/properties/relations.ma   |   8 +-
 3 files changed, 71 insertions(+), 71 deletions(-)

diff --git a/matita/matita/nlibrary/logic/connectives.ma b/matita/matita/nlibrary/logic/connectives.ma
index 4d085995d..ea4642e90 100644
--- a/matita/matita/nlibrary/logic/connectives.ma
+++ b/matita/matita/nlibrary/logic/connectives.ma
@@ -14,43 +14,43 @@
 
 include "logic/pts.ma".
 
-ninductive True: CProp[0] ≝
+inductive True: CProp[0] ≝
   I : True.
 
-ninductive False: CProp[0] ≝.
+inductive False: CProp[0] ≝.
 
-ndefinition Not: CProp[0] → CProp[0] ≝
+definition Not: CProp[0] → CProp[0] ≝
   λA. A → False.
 
-interpretation "logical not" 'not x = (Not x).
+interpretation "logical ot" 'not x = (Not x).
 
-ninductive And (A,B:CProp[0]) : CProp[0] ≝
+inductive And (A,B:CProp[0]) : CProp[0] ≝
     conj : A → B → And A B.
 
 interpretation "logical and" 'and x y = (And x y).
 
-ninductive Or (A,B:CProp[0]) : CProp[0] ≝
+inductive Or (A,B:CProp[0]) : CProp[0] ≝
      or_introl : A → Or A B
    | or_intror : B → Or A B.
 
 interpretation "logical or" 'or x y = (Or x y).
 
-ninductive Ex (A:Type[0]) (P:A → CProp[0]) : CProp[0] ≝
+inductive Ex (A:Type[0]) (P:A → CProp[0]) : CProp[0] ≝
     ex_intro: ∀x:A. P x → Ex A P.
 
 
-ninductive Ex1 (A:Type[1]) (P:A → CProp[0]) : CProp[1] ≝
+inductive Ex1 (A:Type[1]) (P:A → CProp[0]) : CProp[1] ≝
     ex_intro1: ∀x:A. P x → Ex1 A P.
 
 interpretation "exists1" 'exists x = (Ex1 ? x).
 interpretation "exists" 'exists x = (Ex ? x).
 
-ninductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝ 
+inductive sigma (A : Type[0]) (P : A → CProp[0]) : Type[0] ≝ 
  sig_intro : ∀x:A.P x → sigma A P. 
 
 interpretation "sigma" 'sigma \eta.p = (sigma ? p). 
 
-nrecord iff (A,B: CProp[0]) : CProp[0] ≝
+record iff (A,B: CProp[0]) : CProp[0] ≝
  { if: A → B;
    fi: B → A
  }.
diff --git a/matita/matita/nlibrary/logic/equality.ma b/matita/matita/nlibrary/logic/equality.ma
index fa93f4f1b..dfc203e1d 100644
--- a/matita/matita/nlibrary/logic/equality.ma
+++ b/matita/matita/nlibrary/logic/equality.ma
@@ -15,43 +15,43 @@
 include "logic/connectives.ma".
 include "properties/relations.ma".
 
-ninductive eq (A: Type[0]) (a: A) : A → CProp[0] ≝
+inductive eq (A: Type[0]) (a: A) : A → CProp[0] ≝
  refl: eq A a a.
 
-nlemma eq_rect_Type0_r':
+lemma eq_rect_Type0_r':
  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
- #A; #a; #x; #p; ncases p; #P; #H; nassumption.
-nqed.
+ #A; #a; #x; #p; cases p; #P; #H; assumption.
+qed.
 
-nlemma eq_rect_Type0_r:
+lemma eq_rect_Type0_r:
  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption.
-nqed.
+ #A; #a; #P; #p; #x0; #p0; apply (eq_rect_Type0_r' ??? p0); assumption.
+qed.
 
-nlemma eq_rect_CProp0_r':
+lemma eq_rect_CProp0_r':
  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
- #A; #a; #x; #p; ncases p; #P; #H; nassumption.
-nqed.
+ #A; #a; #x; #p; cases p; #P; #H; assumption.
+qed.
 
-nlemma eq_rect_CProp0_r:
+lemma eq_rect_CProp0_r:
  ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
-nqed.
+ #A; #a; #P; #p; #x0; #p0; apply (eq_rect_CProp0_r' ??? p0); assumption.
+qed.
 
-nlemma eq_ind_r :
+lemma eq_ind_r :
  ∀A.∀a.∀P: ∀x:A. eq ? x a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
-nqed.
+ #A; #a; #P; #p; #x0; #p0; apply (eq_rect_CProp0_r' ??? p0); assumption.
+qed.
 
 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)).
+interpretation "leibnitz's on-equality" 'neq t x y = (Not (eq t x y)).
 
-ndefinition R0 ≝ λT:Type[0].λt:T.t.
+definition R0 ≝ λT:Type[0].λt:T.t.
   
-ndefinition R1 ≝ eq_rect_Type0.
+definition R1 ≝ eq_rect_Type0.
 
-ndefinition R2 :
+definition R2 :
   ∀T0:Type[0].
   ∀a0:T0.
   ∀T1:∀x0:T0. a0=x0 → Type[0].
@@ -64,12 +64,12 @@ ndefinition R2 :
   ∀e1:R1 ?? T1 a1 ? e0 = b1.
   T2 b0 e0 b1 e1.
 #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
-napply (eq_rect_Type0 ????? e1);
-napply (R1 ?? ? ?? e0);
-napply a2;
-nqed.
+apply (eq_rect_Type0 ????? e1);
+apply (R1 ?? ? ?? e0);
+apply a2;
+qed.
 
-ndefinition R3 :
+definition R3 :
   ∀T0:Type[0].
   ∀a0:T0.
   ∀T1:∀x0:T0. a0=x0 → Type[0].
@@ -87,12 +87,12 @@ ndefinition R3 :
   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
   T3 b0 e0 b1 e1 b2 e2.
 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
-napply (eq_rect_Type0 ????? e2);
-napply (R2 ?? ? ???? e0 ? e1);
-napply a3;
-nqed.
+apply (eq_rect_Type0 ????? e2);
+apply (R2 ?? ? ???? e0 ? e1);
+apply a3;
+qed.
 
-ndefinition R4 :
+definition R4 :
   ∀T0:Type[0].
   ∀a0:T0.
   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
@@ -122,36 +122,36 @@ ndefinition R4 :
   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
-napply (eq_rect_Type0 ????? e3);
-napply (R3 ????????? e0 ? e1 ? e2);
-napply a4;
-nqed.
-
-naxiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. 
-
-ndefinition EQ: ∀A:Type[0]. equivalence_relation A.
- #A; napply mk_equivalence_relation
-  [ napply eq
-  | napply refl
-  | #x; #y; #H; nrewrite < H; napply refl
-  | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption]
-nqed.
-
-naxiom T1 : Type[0].
-naxiom T2 : T1 → Type[0].
-naxiom t1 : T1.
-naxiom t2 : ∀x:T1. T2 x.
-
-ninductive I2 : ∀r1:T1.T2 r1 → Type[0] ≝ 
+apply (eq_rect_Type0 ????? e3);
+apply (R3 ????????? e0 ? e1 ? e2);
+apply a4;
+qed.
+
+axiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. 
+
+definition EQ: ∀A:Type[0]. equivalence_relation A.
+ #A; apply mk_equivalence_relation
+  [ apply eq
+  | apply refl
+  | #x; #y; #H; rewrite < H; apply refl
+  | #x; #y; #z; #Hyx; #Hxz; rewrite < Hxz; assumption]
+qed.
+
+axiom T1 : Type[0].
+axiom T2 : T1 → Type[0].
+axiom t1 : T1.
+axiom t2 : ∀x:T1. T2 x.
+
+inductive I2 : ∀r1:T1.T2 r1 → Type[0] ≝ 
 | i2c1 : ∀x1:T1.∀x2:T2 x1. I2 x1 x2
 | i2c2 : I2 t1 (t2 t1).
 
-(* nlemma i2d : ∀a,b.∀x,y:I2 a b.
+(* lemma i2d : ∀a,b.∀x,y:I2 a b.
              ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
              ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.
              Type[2].
 #a;#b;#x;#y;
-napply (
+apply (
 match x return (λr1,r2,r.
                  ∀e1:r1 = a. ∀e2:R1 T1 r1 (λz,p. T2 z) r2 a e1 = b.
                  ∀e :R2 T1 r1 (λz,p. T2 z) r2 (λz1,p1,z2,p2. I2 z1 z2) r a e1 b e2 = y. Type[2]) with 
@@ -164,7 +164,7 @@ match x return (λr1,r2,r.
     [ i2c1 y1 y2 ⇒ ?
     | i2c2 ⇒ ? ])
  [#e1; #e2; #e;
-  napply (∀P:Type[1].
+  apply (∀P:Type[1].
                      (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2.
                       ∀f: R2 T1 x1 (λz,p.T2 z) x2
                           (λz1,p1,z2,p2.eq ? 
@@ -179,7 +179,7 @@ match x return (λr1,r2,r.
   *)                          (i2c1 y1 y2)) 
                           ? y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P) 
                    → P);
-  napply (∀P:Type[1].
+  apply (∀P:Type[1].
                      (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2. 
                       ∀f: R2 T1 x1 (λz,p.T2 z) x2
                           (λz1,p1,z2,p2.eq (I2 y1 y2) 
@@ -193,7 +193,7 @@ match x return (λr1,r2,r.
 
 
 
-ndefinition i2d : ∀a,b.∀x,y:I2 a b.
+definition i2d : ∀a,b.∀x,y:I2 a b.
                   ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
                   ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.Type[2] ≝
 λa,b,x,y. 
@@ -226,4 +226,4 @@ match x return (λr1,r2,r.
                     (λz1,p1,z2,p2.eq ? i2c2 i2c2) 
                     e ? e1 ? e2 = refl ? i2c2.P) → P ] ].
 
-*)
\ No newline at end of file
+*)
diff --git a/matita/matita/nlibrary/properties/relations.ma b/matita/matita/nlibrary/properties/relations.ma
index 581208d9a..1df2e205a 100644
--- a/matita/matita/nlibrary/properties/relations.ma
+++ b/matita/matita/nlibrary/properties/relations.ma
@@ -14,11 +14,11 @@
 
 include "logic/pts.ma".
 
-ndefinition reflexive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x.P x x.
-ndefinition symmetric ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x,y.P x y → P y x.
-ndefinition transitive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀z,x,y. P x z → P z y → P x y.
+definition reflexive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x.P x x.
+definition symmetric ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x,y.P x y → P y x.
+definition transitive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀z,x,y. P x z → P z y → P x y.
 
-nrecord equivalence_relation (A:Type[0]) : Type[1] ≝
+record equivalence_relation (A:Type[0]) : Type[1] ≝
  { eq_rel:2> A → A → CProp[0];
    refl: reflexive ? eq_rel;
    sym: symmetric ? eq_rel;
-- 
2.39.2