1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "datatypes/list.ma".
16 include "sets/setoids.ma".
18 nlet rec eq_list (A : setoid) (l1, l2 : list A) on l1 : CProp[0] ≝
20 [ nil ⇒ match l2 return λ_.CProp[0] with [ nil ⇒ True | _ ⇒ False ]
21 | cons x xs ⇒ match l2 with [ nil ⇒ False | cons y ys ⇒ x = y ∧ eq_list ? xs ys]].
23 interpretation "eq_list" 'eq_low a b = (eq_list ? a b).
25 ndefinition LIST : setoid → setoid.
26 #S; @(list S); @(eq_list S);
27 ##[ #l; nelim l; //; #; @; //;
28 ##| #l1; nelim l1; ##[ #y; ncases y; //] #x xs H y; ncases y; ##[*] #y ys; *; #; @; /2/;
29 ##| #l1; nelim l1; ##[ #l2 l3; ncases l2; ncases l3; /3/; #z zs y ys; *]
30 #x xs H l2 l3; ncases l2; ncases l3; /2/; #z zs y yz; *; #H1 H2; *; #H3 H4; @; /3/;##]
33 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
34 unification hint 0 ≔ S : setoid;
36 P1 ≟ refl ? (eq0 (LIST S)),
37 P2 ≟ sym ? (eq0 (LIST S)),
38 P3 ≟ trans ? (eq0 (LIST S)),
39 X ≟ mk_setoid (list (carr S)) (mk_equivalence_relation ? (eq_list S) P1 P2 P3)
40 (*-----------------------------------------------------------------------*) ⊢
43 unification hint 0 ≔ S:setoid, a,b:list (carr S);
46 (* -------------------------------------------- *) ⊢
47 eq_list S a b ≡ eq_rel L R a b.
49 nlemma append_is_morph : ∀A:setoid.(list A) ⇒_0 (list A) ⇒_0 (list A).
50 #A; napply (mk_binary_morphism … (λs1,s2:list A. s1 @ s2)); #a; nelim a;
51 ##[ #l1 l2 l3 defl1 El2l3; ncases l1 in defl1; ##[#;nassumption] #x xs; *;
52 ##| #x xs IH l1 l2 l3 defl1 El2l3; ncases l1 in defl1; ##[ *] #y ys; *; #; /3/]
55 alias symbol "hint_decl" (instance 1) = "hint_decl_Type0".
56 unification hint 0 ≔ S:setoid, A,B:list (carr S);
58 MM ≟ mk_unary_morphism ?? (λA:list (carr S).
60 (λB:list (carr S).A @ B) (prop1 ?? (fun1 ??(append_is_morph S) A)))
61 (prop1 ?? (append_is_morph S)),
63 (*--------------------------------------------------------------------------*) ⊢
64 fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ append SS A B.
67 (* XXX to understand if are always needed or only if the coercion is active *)
68 include "sets/setoids1.ma".
70 unification hint 0 ≔ SS : setoid;
72 TT ≟ setoid1_of_setoid (LIST SS)
73 (*-----------------------------------------------------------------*) ⊢
76 alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
77 unification hint 0 ≔ S : setoid, x,y;
79 TT ≟ setoid1_of_setoid SS
80 (*-----------------------------------------*) ⊢
81 eq_list S x y ≡ eq_rel1 ? (eq1 TT) x y.