helm/software/matita/nlibrary/datatypes/list-setoids.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "datatypes/list.ma".
  16 include "sets/setoids.ma".
  17
  18 nlet rec eq_list (A : setoid) (l1, l2 : list A) on l1 : CProp[0] ≝
  19 match l1 with
  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]].
  22
  23 interpretation "eq_list" 'eq_low a b = (eq_list ? a b).
  24
  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/;##]
  31 nqed.
  32
  33 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
  34 unification hint 0 ≔ S : setoid;
  35   T ≟ carr S,
  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 (*-----------------------------------------------------------------------*) ⊢
  41      carr X ≡ list T.
  42
  43 unification hint 0 ≔ S:setoid, a,b:list (carr S);
  44    R ≟ eq0 (LIST S),
  45    L ≟ (list (carr S))
  46 (* -------------------------------------------- *) ⊢
  47    eq_list S a b ≡ eq_rel L R a b.
  48
  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/]
  53 nqed.
  54
  55 alias symbol "hint_decl" (instance 1) = "hint_decl_Type0".
  56 unification hint 0 ≔ S:setoid, A,B:list (carr S);
  57     SS ≟ carr S,
  58     MM ≟ mk_unary_morphism ?? (λA:list (carr S).
  59             mk_unary_morphism ??
  60               (λB:list (carr S).A @ B) (prop1 ?? (fun1 ??(append_is_morph S) A)))
  61           (prop1 ?? (append_is_morph S)),
  62     T ≟ LIST S
  63 (*--------------------------------------------------------------------------*) ⊢
  64    fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ append SS A B.
  65
  66
  67 (* XXX to understand if are always needed or only if the coercion is active *)
  68 include "sets/setoids1.ma".
  69
  70 unification hint 0 ≔ SS : setoid;
  71   S ≟ carr SS,
  72   TT ≟ setoid1_of_setoid (LIST SS)
  73 (*-----------------------------------------------------------------*) ⊢
  74   list S ≡ carr1 TT.
  75
  76 alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
  77 unification hint 0 ≔ S : setoid, x,y;
  78   SS ≟ LIST S,
  79   TT ≟ setoid1_of_setoid SS
  80 (*-----------------------------------------*) ⊢
  81   eq_list S x y ≡ eq_rel1 ? (eq1 TT) x y.
  82