matita/matita/lib/basics/deqlist.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_______________________________________________________________ *)
  11
  12 include "basics/deqsets.ma".
  13 include "basics/lists/listb.ma".
  14
  15 (*
  16
  17 record DeqSet : Type[1] ≝ {
  18    carr :> Type[0];
  19    eqb: carr → carr → bool;
  20    eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
  21 }. *)
  22
  23
  24 (* list *)
  25
  26 let rec eq_list (A:DeqSet) (l1,l2:list A) on l1 ≝
  27   match l1 with
  28   [ nil ⇒ match l2 with [nil ⇒ true | _ ⇒ false]
  29   | cons a1 tl1 ⇒
  30       match l2 with [nil ⇒ false | cons a2 tl2 ⇒ a1 ==a2 ∧ eq_list A tl1 tl2]].
  31
  32 lemma eq_list_true: ∀A:DeqSet.∀l1,l2:list A.
  33   eq_list A l1 l2 = true ↔ l1 = l2.
  34 #A #l1 elim l1
  35   [* [% // |#a #tl % normalize #H destruct ]
  36   |#a1 #tl1 #Hind *
  37     [normalize % #H destruct
  38     |#a2 #tl2 normalize %
  39       [cases (true_or_false (a1==a2)) #Heq >Heq normalize
  40         [#Htl >(\P Heq) >(proj1 … (Hind tl2) Htl) // | #H destruct ]
  41       |#H destruct >(\b (refl … )) >(proj2 … (Hind tl2) (refl …)) //
  42       ]
  43     ]
  44   ]
  45 qed.
  46
  47 definition DeqList ≝ λA:DeqSet.
  48   mk_DeqSet (list A) (eq_list A) (eq_list_true A).
  49
  50 unification hint  0 ≔ C;
  51     T ≟ carr C,
  52     X ≟ DeqList C
  53 (* ---------------------------------------- *) ⊢
  54     list T ≡ carr X.
  55
  56 alias id "eqb" = "cic:/matita/basics/deqsets/eqb#fix:0:0:3".
  57 alias symbol "hint_decl" (instance 1) = "hint_decl_Type0".
  58 unification hint  0 ≔ T,a1,a2;
  59     X ≟ DeqList T
  60 (* ---------------------------------------- *) ⊢
  61     eq_list T a1 a2 ≡ eqb X a1 a2.
  62
  63