matita/matita/lib/binding/names.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 "basics/logic.ma".
  16 include "basics/lists/in.ma".
  17 include "basics/types.ma".
  18
  19 (*interpretation "list membership" 'mem x l = (in_list ? x l).*)
  20
  21 record Nset : Type[1] ≝
  22 {
  23   (* carrier is specified as a coercion: when an object X of type Nset is
  24      given, but something of type Type is expected, Matita will insert a
  25      hidden coercion: the user sees "X", but really means "carrier X"     *)
  26   carrier :> DeqSet;
  27   N_fresh : list carrier → carrier;
  28   p_fresh : ∀l.N_fresh l ∉ l
  29 }.
  30
  31 definition maxlist ≝
  32  λl.foldr ?? (λx,acc.max x acc) 0 l.
  33
  34 definition natfresh ≝ λl.S (maxlist l).
  35
  36 lemma le_max_1 : ∀x,y.x ≤ max x y. /2/
  37 qed.
  38
  39 lemma le_max_2 : ∀x,y.y ≤ max x y. /2/
  40 qed.
  41
  42 lemma le_maxlist : ∀l,x.x ∈ l → x ≤ maxlist l.
  43 #l elim l
  44 [#x #Hx @False_ind cases (not_in_list_nil ? x) #H1 /2/
  45 |#y #tl #IH #x #H1 change with (max ??) in ⊢ (??%);
  46  cases (in_list_cons_case ???? H1);#H2;
  47  [ >H2 @le_max_1
  48  | whd in ⊢ (??%); lapply (refl ? (leb y (maxlist tl)));
  49    cases (leb y (maxlist tl)) in ⊢ (???% → %);#H3
  50    [ @IH //
  51    | lapply (IH ? H2) #H4
  52      lapply (leb_false_to_not_le … H3) #H5
  53      lapply (not_le_to_lt … H5) #H6
  54      @(transitive_le … H4)
  55      @(transitive_le … H6) %2 %
  56    ]
  57  ]
  58 ]
  59 qed.
  60
  61 (* prove freshness for nat *)
  62 lemma lt_l_natfresh_l : ∀l,x.x ∈ l → x < natfresh l.
  63 #l #x #H1 @le_S_S /2/
  64 qed.
  65
  66 (*naxiom p_Xfresh : ∀l.∀x:Xcarr.x ∈ l → x ≠ ntm (Xfresh l) ∧ x ≠ ntp (Xfresh l).*)
  67 lemma p_natfresh : ∀l.natfresh l ∉ l.
  68 #l % #H1 lapply (lt_l_natfresh_l … H1) #H2
  69 cases (lt_to_not_eq … H2) #H3 @H3 %
  70 qed.
  71
  72 include "basics/finset.ma".
  73
  74 definition X : Nset ≝ mk_Nset DeqNat ….
  75 [ @natfresh
  76 | @p_natfresh
  77 ]
  78 qed.