From a4cd6a8a1d6a008518c12daca794b9e811c1dee5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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