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
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.
(* ---------------------------------------- *) ⊢
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
| 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).
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}.
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 ⇒ { [ ] }
| 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
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).
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
projects / helm.git / commitdiff