(*-----------------------------------------------------------------------*) ⊢
carr X ≡ list T.
+unification hint 0 ≔ S,a,b;
+ R ≟ LIST S,
+ L ≟ (list S)
+(* -------------------------------------------- *) ⊢
+ eq_list S a b ≡ eq_rel L (eq0 R) a b.
+
notation "hvbox(hd break :: tl)"
right associative with precedence 47
for @{'cons $hd $tl}.
ndefinition associative ≝ λA:setoid.λf:A → A → A.∀x,y,z.f x (f y z) = f (f x y) z.
-ninductive one : Type[0] ≝ unit : one.
-
-ndefinition force ≝
- λS:Type[2].λs:S.λT:Type[2].λt:T.λlock:one.
- match lock return λ_.Type[2] with [ unit ⇒ T].
-
-nlet rec lift (S:Type[2]) (s:S) (T:Type[2]) (t:T) (lock:one) on lock : force S s T t lock ≝
- match lock return λlock.force S s T t lock with [ unit ⇒ t ].
-
-ncoercion lift1 : ∀S:Type[1].∀s:S.∀T:Type[1].∀t:T.∀lock:one. force S s T t lock ≝ lift
- on s : ? to force ?????.
-
-ncoercion lift2 : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock ≝ lift
- on s : ? to force ?????.
-
-unification hint 0 ≔ R : setoid;
- TR ≟ setoid, MR ≟ (carr R), lock ≟ unit
-(* ---------------------------------------- *) ⊢
- setoid ≡ force ?(*Type[0]*) MR TR R lock.
-
-unification hint 0 ≔ R : setoid1;
- TR ≟ setoid1, MR ≟ (carr1 R), lock ≟ unit
-(* ---------------------------------------- *) ⊢
- setoid1 ≡ force ? MR TR R lock.
ntheorem associative_append: ∀A:setoid.associative (list A) (append A).
-#A;#x;#y;#z;nelim x[//|#a;#x1;#H;nnormalize;/2/]nqed.
+#A;#x;#y;#z;nelim x[ napply # |#a;#x1;#H;nnormalize;/2/]nqed.
interpretation "iff" 'iff a b = (iff a b).
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ bool.
+unification hint 0 ≔ a,b;
+ R ≟ BOOL,
+ L ≟ bool
+(* -------------------------------------------- *) ⊢
+ eq bool a b ≡ eq_rel L (eq0 R) a b.
+
nrecord Alpha : Type[1] ≝ {
acarr :> setoid;
eqb: acarr → acarr → bool;
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ (re T).
+unification hint 0 ≔ A,a,b;
+ R ≟ RE A,
+ L ≟ re A
+(* -------------------------------------------- *) ⊢
+ eq_re A a b ≡ eq_rel L (eq0 R) a b.
+
notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}.
interpretation "star" 'pk a = (k ? a).
notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
interpretation "epsilon" 'epsilon = (e ?).
-notation "0" non associative with precedence 90 for @{ 'empty }.
-interpretation "empty" 'empty = (z ?).
+notation "0" non associative with precedence 90 for @{ 'empty_r }.
+interpretation "empty" 'empty_r = (z ?).
notation > "'lang' S" non associative with precedence 90 for @{ Ω^(list $S) }.
notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(list $S) }.
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_set : ∀A.Ω^A ≝ λA.{ w | False }.
-notation "∅" non associative with precedence 90 for @{'emptyset}.
-interpretation "empty set" 'emptyset = (empty_set ?).
-
-(*
-notation "{}" non associative with precedence 90 for @{'empty_lang}.
-interpretation "empty lang" 'empty_lang = (empty_lang ?).
-*)
-
ndefinition sing_lang : ∀A:setoid.∀x:A.Ω^A ≝ λS.λx.{ w | x = w }.
interpretation "sing lang" 'singl x = (sing_lang ? x).
ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S ≝ pc on _p : pitem ? to ∀_:?.?.
interpretation "patom" 'ps a = (ps ? a).
interpretation "pepsilon" 'epsilon = (pe ?).
-interpretation "pempty" 'empty = (pz ?).
+interpretation "pempty" 'empty_r = (pz ?).
notation > "|term 19 e|" non associative with precedence 70 for @{forget ? $e}.
nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'L_pi $E}.
interpretation "in_pl" 'L_pi E = (L_pi ? E).
-unification hint 0 ≔ S,a,b;
- R ≟ LIST S,
- L ≟ (list S)
-(* -------------------------------------------- *) ⊢
- eq_list S a b ≡ eq_rel L (eq0 R) a b.
-
+(* The caml, as some patches for it *)
ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
(*-----------------------------------------------------------------*) ⊢
list S ≡ carr1 TT.
-
+(* Ex setoid support *)
nlemma Sig: ∀S,T:setoid.∀P: S → (T → CPROP).
∀y,z:T.y = z → (∀x.y=z → P x y = P x z) → (Ex S (λx.P x y)) =_1 (Ex S (λx.P x z)).
#S T P y z Q E; @; *; #x Px; @x; nlapply (E x Q); *; /2/; nqed.
napply (.=_1 (∑ E (λw,H.(H ╪_1 #) ╪_1 #)) ╪_1 #).
napply #.
nqed.
+(* Ex setoid support end *)
ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
#S r; @(𝐋\p r); #w1 w2 E; nelim r;
ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
interpretation "reclose" 'eclose x = (reclose ? x).
-nlemma cup0 :∀S.∀p:lang S.p ∪ ∅ = p.
-#S p; @; #w; ##[*; //| #; @1; //] *; nqed.
-
-nlemma cupC : ∀S. ∀a,b:lang S.a ∪ b = b ∪ a.
-#S a b; @; #w; *; nnormalize; /2/; nqed.
-
-nlemma cupID : ∀S. ∀a:lang S.a ∪ a = a.
-#S a; @; #w; ##[*; //] /2/; nqed.
-
nlemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) = ϵ b1 ∪ ϵ b2. ##[##2: napply S]
#S b1 b2; ncases b1; ncases b2;
nchange in match (true || true) with true;
nchange in match (ϵ true) with {[]};
nchange in match (ϵ false) with ∅;
##[##1,4: napply ((cupID…)^-1);
-##| napply ((cup0 S {[]})^-1);
-##| napply (.= (cup0 S {[]})^-1); napply cupC; ##]
+##| napply ((cup0 ? {[]})^-1);
+##| napply (.= (cup0 ? {[]})^-1); napply cupC; ##]
nqed.
-nlemma cupA : ∀S.∀a,b,c:lang S.a ∪ b ∪ c = a ∪ (b ∪ c).
-#S a b c; @; #w; *; /3/; *; /3/; nqed.
-
+(* XXX move somewere else *)
ndefinition if': ∀A,B:CPROP. A = B → A → B.
#A B; *; /2/. nqed.
projects / helm.git / blobdiff