From a4cd6a8a1d6a008518c12daca794b9e811c1dee5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 21 Jul 2010 08:54:04 +0000
Subject: [PATCH] ...

---
 .../software/matita/nlibrary/re/re-setoids.ma | 109 +++++++++++-------
 1 file changed, 68 insertions(+), 41 deletions(-)

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index 561ff9d6a..a47d6defa 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -19,26 +19,27 @@ include "logic/cprop.ma".
 ninductive Admit : CProp[0] ≝ .
 naxiom admit : Admit.
 
-ninductive list (A:setoid) : Type[0] ≝ 
+ninductive list (A:Type[0]) : Type[0] ≝ 
   | nil: list A
   | cons: A -> list A -> list A.
   
-nlet rec eq_list A (l1, l2 : list A) on l1 : CProp[0] ≝ 
+nlet rec eq_list (A : setoid) (l1, l2 : list A) on l1 : CProp[0] ≝ 
 match l1 with
-[ nil ⇒ match l2 with [ nil ⇒ ? | _ ⇒ ? ]
+[ nil ⇒ match l2 return λ_.CProp[0] with [ nil ⇒ ? | _ ⇒ ? ]
 | cons x xs ⇒ match l2 with [ nil ⇒ ? | cons y ys ⇒ x = y ∧ eq_list ? xs ys]].
 ##[ napply True|napply False|napply False]nqed.
    
 ndefinition LIST : setoid → setoid.
 #S; @(list S); @(eq_list S); ncases admit; nqed.  
 
-unification hint 0 ≔ S;
+unification hint 0 ≔ S : setoid;
+  T ≟ carr S,
   P1 ≟ refl ? (eq (LIST S)),
   P2 ≟ sym ? (eq (LIST S)),
   P3 ≟ trans ? (eq (LIST S)),
   X ≟ mk_setoid (list S) (mk_equivalence_relation ? (eq_list S) P1 P2 P3)
 (*-----------------------------------------------------------------------*) ⊢
-     carr X ≡ list S.
+     carr X ≡ list T.
 
 notation "hvbox(hd break :: tl)"
   right associative with precedence 47
@@ -62,7 +63,7 @@ nlet rec append A (l1: list A) l2 on l1 ≝
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
-ntheorem append_nil: ∀A.∀l:list A.l @ [] = l.
+ntheorem append_nil: ∀A:setoid.∀l:list A.l @ [] = l.
 #A;#l;nelim l;//; #a;#l1;#IH;nnormalize;/2/;nqed.
 
 ndefinition associative ≝ λA:setoid.λf:A → A → A.∀x,y,z.f x (f y z) = f (f x y) z. 
@@ -84,23 +85,33 @@ unification hint 0 ≔ R : setoid;
 (* ---------------------------------------- *) ⊢ 
    setoid ≡ force ?(*Type[0]*) MR TR R lock.
 
-ntheorem associative_append: ∀A.associative (list A) (append A).
+ntheorem associative_append: ∀A:setoid.associative (list A) (append A).
 #A;#x;#y;#z;nelim x[//|#a;#x1;#H;nnormalize;/2/]nqed.
 
 interpretation "iff" 'iff a b = (iff a b).  
 
+naxiom eq_bool : bool → bool → CProp[0].
+ndefinition BOOL : setoid.
+@bool; @eq_bool; ncases admit.nqed.
+
+unification hint 0 ≔ ;
+  P1 ≟ refl ? (eq BOOL),
+  P2 ≟ sym ? (eq BOOL),
+  P3 ≟ trans ? (eq BOOL),
+  X ≟ mk_setoid bool (mk_equivalence_relation ? eq_bool P1 P2 P3)
+(*-----------------------------------------------------------------------*) ⊢
+     carr X ≡ bool.
+
 nrecord Alpha : Type[1] ≝ { 
-   carr :> setoid;
-   eqb: carr → carr → bool; (*
-   eqb_true: ∀x,y. (eqb x y = true) = (x = y) *)
+   acarr :> setoid;
+   eqb: acarr → acarr → bool (*; 
+   eqb_true: ∀x,y. (eqb x y = true) = (x = y)*)
 }.
  
 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
 interpretation "eqb" 'eqb a b = (eqb ? a b).
 
-ndefinition word ≝ λS:Alpha.list S.
-
-ninductive re (S: Alpha) : Type[0] ≝
+ninductive re (S: Type[0]) : Type[0] ≝
    z: re S
  | e: re S
  | s: S → re S
@@ -108,6 +119,21 @@ ninductive re (S: Alpha) : Type[0] ≝
  | o: re S → re S → re S
  | k: re S → re S.
  
+naxiom eq_re : ∀S:Alpha.re S → re S → CProp[0].
+ndefinition RE : Alpha → setoid.
+#A; @(re A); @(eq_re A); ncases admit. nqed.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+alias id "carr" = "cic:/matita/ng/sets/setoids/carr.fix(0,0,1)".
+unification hint 0 ≔ A : Alpha;
+  T ≟ acarr A,
+  P1 ≟ refl ? (eq (RE A)),
+  P2 ≟ sym ? (eq (RE A)),
+  P3 ≟ trans ? (eq (RE A)),
+  X ≟ mk_setoid (re T) (mk_equivalence_relation ? (eq_re A) P1 P2 P3)
+(*-----------------------------------------------------------------------*) ⊢
+     carr X ≡ (re T).
+
 notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
 notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
 interpretation "star" 'pk a = (k ? a).
@@ -117,7 +143,7 @@ notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
 interpretation "cat" 'pc a b = (c ? a b).
 
 (* to get rid of \middot *)
-ncoercion c  : ∀S:Alpha.∀p:re S.  re S →  re S   ≝ c  on _p : re ?  to ∀_:?.?.
+ncoercion c  : ∀S.∀p:re S.  re S →  re S   ≝ c  on _p : re ?  to ∀_:?.?.
 
 notation < "a" non associative with precedence 90 for @{ 'ps $a}.
 notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
@@ -129,32 +155,38 @@ interpretation "epsilon" 'epsilon = (e ?).
 notation "∅" non associative with precedence 90 for @{ 'empty }.
 interpretation "empty" 'empty = (z ?).
 
-nlet rec flatten (S : Alpha) (l : list (word S)) on l : word S ≝ 
+nrecord Setl (A : Type[0]) : Type[1] ≝ { in_set : A → CProp[0] }. 
+ndefinition Lang ≝ λA.Setl (list A).
+
+interpretation "in Setl" 'mem x l = (in_set ? l x).
+interpretation "compr Lang" 'comprehension t f = (mk_Setl t f).
+
+nlet rec flatten S (l : list (list S)) on l : list S ≝ 
 match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
 
-nlet rec conjunct (S : Alpha) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
-match l with [ nil ⇒ ? | cons w tl ⇒ r w ∧ conjunct ? tl r ]. napply True. nqed.
+nlet rec conjunct S (l : list (list S)) (L : Lang S) on l: CProp[0] ≝
+match l with [ nil ⇒ True | cons w tl ⇒ w ∈ L ∧ conjunct ? tl L ].
 
-ndefinition empty_lang ≝ λS.λw:word S.False.
+ndefinition empty_lang ≝ λS.{ w ∈ list S | False }.
 notation "{}" non associative with precedence 90 for @{'empty_lang}.
 interpretation "empty lang" 'empty_lang = (empty_lang ?).
 
-ndefinition sing_lang ≝ λS.λx,w:word S.x=w.
-notation "{x}" non associative with precedence 90 for @{'sing_lang $x}.
-interpretation "sing lang" 'sing_lang x = (sing_lang ? x).
+ndefinition sing_lang ≝ λS:Alpha.λx.{ w ∈ list S | x = w }.
+interpretation "sing lang" 'singl x = (sing_lang ? x).
 
-ndefinition union : ∀S,l1,l2,w.Prop ≝ λS.λl1,l2.λw:word S.l1 w ∨ l2 w.
+ndefinition union ≝ λS.λl1,l2.{ w ∈ list S | w ∈ l1 ∨ w ∈ l2}.
 interpretation "union lang" 'union a b = (union ? a b).
 
-ndefinition cat : ∀S,l1,l2,w.Prop ≝ 
-  λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
+ndefinition cat ≝ 
+  λS:Alpha.λl1,l2.{ w ∈ list S | ∃w1,w2.w1 @ w2 = w ∧ w1 ∈ l1 ∧ w2 ∈ l2}.
 interpretation "cat lang" 'pc a b = (cat ? a b).
 
-ndefinition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l. 
+ndefinition star ≝ 
+  λS:Alpha.λl.{ w ∈ list S | ∃lw.flatten ? lw = w ∧ conjunct ? lw l}. 
 interpretation "star lang" 'pk l = (star ? l).
 
-notation > "𝐋 term 90 E" non associative with precedence 90 for @{in_l ? $E}.
-nlet rec in_l (S : Alpha) (r : re S) on r : word S → Prop ≝ 
+notation > "𝐋 term 90 E" non associative with precedence 75 for @{L_re ? $E}.
+nlet rec L_re (S : Alpha) (r : re S) on r : Lang S ≝ 
 match r with
 [ z ⇒ {}
 | e ⇒ { [ ] }
@@ -162,19 +194,14 @@ match r with
 | c r1 r2 ⇒ 𝐋 r1 · 𝐋 r2
 | o r1 r2 ⇒  𝐋 r1 ∪ 𝐋 r2
 | k r1 ⇒ (𝐋 r1) ^*].
-notation "𝐋 term 90 E" non associative with precedence 90 for @{'in_l $E}.
-interpretation "in_l" 'in_l E = (in_l ? E).
-interpretation "in_l mem" 'mem w l = (in_l ? l w).
+notation "𝐋 term 90 E" non associative with precedence 75 for @{'L_re $E}.
+interpretation "in_l" 'L_re E = (L_re ? E).
 
 notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
+ndefinition orb ≝ λa,b:bool. match a with [ true ⇒ true | _ ⇒ b ].
 interpretation "orb" 'orb a b = (orb a b).
 
-ndefinition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
-notation > "'if' term 19 e 'then' term 19 t 'else' term 19 f" non associative with precedence 19 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 19 for @{ 'if_then_else $e $t $f }.
-interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
-
-ninductive pitem (S: Alpha) : Type[0] ≝
+ninductive pitem (S: Type[0]) : Type[0] ≝
    pz: pitem S
  | pe: pitem S
  | ps: S → pitem S
@@ -185,6 +212,11 @@ ninductive pitem (S: Alpha) : Type[0] ≝
  
 ndefinition pre ≝ λS.pitem S × bool.
 
+notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
+interpretation "fst" 'fst x = (fst ? ? x).
+notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
+interpretation "snd" 'snd x = (snd ? ? x).
+
 interpretation "pstar" 'pk a = (pk ? a).
 interpretation "por" 'plus a b = (po ? a b).
 interpretation "pcat" 'pc a b = (pc ? a b).
@@ -210,11 +242,6 @@ nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
 notation < ".|term 19 e|" non associative with precedence 70 for @{'forget $e}.
 interpretation "forget" 'forget a = (forget ? a).
 
-notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
-interpretation "fst" 'fst x = (fst ? ? x).
-notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}.
-interpretation "snd" 'snd x = (snd ? ? x).
-
 notation > "𝐋\p\ term 90 E" non associative with precedence 90 for @{in_pl ? $E}.
 nlet rec in_pl (S : Alpha) (r : pitem S) on r : word S → Prop ≝ 
 match r with
-- 
2.39.2