helm/software/matita/library/decidable_kit/decidable.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 (* classical connectives for decidable properties *)
  16
  17 include "decidable_kit/streicher.ma".
  18 include "datatypes/bool.ma".
  19 include "logic/connectives.ma".
  20 include "nat/compare.ma".
  21
  22 (* se non includi connectives accade un errore in modo reproducibile*)
  23
  24 (* ### Prop <-> bool reflection predicate and lemmas for switching ### *)
  25 inductive reflect (P : Prop) : bool  → Type ≝
  26   | reflect_true : P → reflect P true
  27   | reflect_false: ¬P → reflect P false.
  28
  29 lemma b2pT : ∀P,b. reflect P b → b = true → P.
  30 intros 3 (P b H);
  31 (* XXX generalize in match H; clear H; rewrite > Db;*)
  32 (* la rewrite pare non andare se non faccio la generalize *)
  33 (* non va inversion: intros (H);inversion H; *)
  34 cases H; [intros; assumption | intros 1 (ABS); destruct ABS ]
  35 qed.
  36
  37 lemma b2pF : ∀P,b. reflect P b → b = false → ¬P.
  38 intros 3 (P b H);
  39 cases H; [intros 1 (ABS); destruct ABS| intros; assumption]
  40 qed.
  41
  42 lemma p2bT : ∀P,b. reflect P b → P → b = true.
  43 intros 4 (P b H Hp);
  44 cases H (Ht Hf); [ intros; reflexivity | cases (Hf Hp)]
  45 qed.
  46
  47 lemma p2bF : ∀P,b. reflect P b → ¬P → b = false.
  48 intros 4 (P b H Hp);
  49 cases H (Ht Hf); [ cases (Hp Ht) | reflexivity ]
  50 qed.
  51
  52 lemma idP : ∀b:bool.reflect (b=true) b.
  53 intros (b); cases b; [ constructor 1; reflexivity | constructor 2;]
  54 unfold Not; intros (H); destruct H;
  55 qed.
  56
  57 lemma prove_reflect : ∀P:Prop.∀b:bool.
  58   (b = true → P) → (b = false → ¬P) → reflect P b.
  59 intros 2 (P b); cases b; intros; [left|right] autobatch.
  60 qed.
  61
  62 (* ### standard connectives/relations with reflection predicate ### *)
  63
  64 definition negb : bool → bool ≝ λb.match b with [ true ⇒ false | false ⇒ true].
  65
  66 lemma negbP : ∀b:bool.reflect (b = false) (negb b).
  67 intros (b); cases b; simplify; [apply reflect_false | apply reflect_true]
  68 [unfold Not; intros (H); destruct H | reflexivity]
  69 qed.
  70
  71 definition andb : bool → bool → bool ≝
  72   λa,b:bool. match a with [ true ⇒ b | false ⇒ false ].
  73
  74 lemma andbP : ∀a,b:bool. reflect (a = true ∧ b = true) (andb a b).
  75 intros (a b); apply prove_reflect; cases a; cases b; simplify; intros (H);
  76 [1,2,3,4: rewrite > H; split; reflexivity;
  77 |5,6,7,8: unfold Not; intros (H1); cases H1;
  78           [destruct H|destruct H3|destruct H2|destruct H2]]
  79 qed.
  80
  81 lemma andbPF : ∀a,b:bool. reflect (a = false ∨ b = false) (negb (andb a b)).
  82 intros (a b); apply prove_reflect; cases a; cases b; simplify; intros (H);
  83 [1,2,3,4: try rewrite > H; [1,2:right|3,4:left] reflexivity
  84 |5,6,7,8: unfold Not; intros (H1); [2,3,4: destruct H]; cases H1; destruct H2]
  85 qed.
  86
  87 definition orb : bool → bool → bool ≝
  88   λa,b.match a in bool with [true ⇒ true | false ⇒ b].
  89
  90 lemma orbP : ∀a,b:bool. reflect (a = true ∨ b = true) (orb a b).
  91 intros (a b); cases a; cases b; simplify;
  92 [1,2,3: apply reflect_true; [1,2: left | right ]; reflexivity
  93 | apply reflect_false; unfold Not; intros (H); cases H (E E); destruct E]
  94 qed.
  95
  96 lemma orbC : ∀a,b. orb a b = orb b a.
  97 intros (a b); cases a; cases b; autobatch. qed.
  98
  99 lemma lebP: ∀x,y. reflect (x ≤ y) (leb x y).
 100 intros (x y); generalize in match (leb_to_Prop x y);
 101 cases (leb x y); simplify; intros (H);
 102 [apply reflect_true | apply reflect_false ] assumption.
 103 qed.
 104
 105 lemma leb_refl : ∀n.leb n n = true.
 106 intros (n); apply (p2bT ? ? (lebP ? ?)); apply le_n; qed.
 107
 108 lemma lebW : ∀n,m. leb (S n) m = true → leb n m = true.
 109 intros (n m H); lapply (b2pT ? ? (lebP ? ?) H); clear H;
 110 apply (p2bT ? ? (lebP ? ?)); apply lt_to_le; assumption.
 111 qed.
 112
 113 definition ltb ≝ λx,y.leb (S x) y.
 114
 115 lemma ltbP: ∀x,y. reflect (x < y) (ltb x y).
 116 intros (x y); apply (lebP (S x) y);
 117 qed.
 118
 119 lemma ltb_refl : ∀n.ltb n n = false.
 120 intros (n); apply (p2bF ? ? (ltbP ? ?)); autobatch;
 121 qed.
 122
 123 (* ### = between booleans as <-> in Prop ### *)
 124 lemma eq_to_bool :
 125   ∀a,b:bool. a = b → (a = true → b = true) ∧ (b = true → a = true).
 126 intros (a b Eab); split; rewrite > Eab; intros; assumption;
 127 qed.
 128
 129 lemma bool_to_eq :
 130   ∀a,b:bool. (a = true → b = true) ∧ (b = true → a = true) → a = b.
 131 intros (a b Eab); decompose;
 132 generalize in match H; generalize in match H1; clear H; clear H1;
 133 cases a; cases b; intros (H1 H2);
 134 [2: rewrite > (H2 ?) | 3: rewrite > (H1 ?)] reflexivity;
 135 qed.
 136
 137
 138 lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m.
 139 intros (n m); apply bool_to_eq; split; intros (H);
 140 [1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch type]
 141    rewrite > (eqb_true_to_eq ? ? H1); autobatch
 142 |2:cases (b2pT ? ? (lebP ? ?) H);
 143    [ elim n; [reflexivity|assumption]
 144    | simplify; rewrite > (p2bT ? ? (lebP ? ?) H1); rewrite > orbC ]
 145    reflexivity]
 146 qed.
 147
 148
 149 (* OUT OF PLACE *)
 150 lemma ltW : ∀n,m. n < m → n < (S m).
 151 intros; unfold lt; unfold lt in H; autobatch. qed.
 152
 153 lemma ltbW : ∀n,m. ltb n m = true → ltb n (S m) = true.
 154 intros (n m H); letin H1 ≝ (b2pT ? ? (ltbP ? ?) H); clearbody H1;
 155 apply (p2bT ? ? (ltbP ? ?) (ltW ? ? H1));
 156 qed.
 157
 158 lemma ltS : ∀n,m.n < m → S n < S m.
 159 intros (n m H); apply (b2pT ? ? (ltbP ? ?)); simplify; apply (p2bT ? ? (ltbP ? ?) H);
 160 qed.
 161
 162 lemma ltS' : ∀n,m.S n < S m → n < m.
 163 intros (n m H); apply (b2pT ? ? (ltbP ? ?)); simplify; apply (p2bT ? ? (ltbP ? ?) H);
 164 qed.
 165
 166 lemma ltb_n_Sm : ∀m.∀n:nat. (orb (ltb n m) (eqb n m)) = ltb n (S m).
 167 intros (m n); apply bool_to_eq; split;
 168 [1: intros; cases (b2pT ? ? (orbP ? ?) H); [1: apply ltbW; assumption]
 169     rewrite > (eqb_true_to_eq ? ? H1); simplify;
 170     rewrite > leb_refl; reflexivity
 171 |2: elim n in m ⊢ % 0;
 172     [1: simplify; intros; cases n1; reflexivity;
 173     |2: intros 1 (m); elim m 0;
 174         [1: intros; apply (p2bT ? ? (orbP ? ?));
 175             lapply (H (pred n1) ?); [1: reflexivity] clear H;
 176             generalize in match H1;
 177             generalize in match Hletin;
 178             cases n1; [1: simplify; intros; destruct H2]
 179             intros; unfold pred in H; simplify in H;
 180             cases (b2pT ? ? (orbP ? ?) H); [left|right] assumption;
 181         |2: clear m; intros (m IH1 IH2 w);
 182             lapply (IH1 ? (pred w));
 183             [3: generalize in match H; cases w; [2: intros; assumption]
 184                 simplify; intros; destruct H1;
 185             |1: intros; apply (IH2 (S n1)); assumption;
 186             |2: generalize in match H; generalize in match Hletin;
 187                 cases w; [1: simplify; intros; destruct H2]
 188                 intros (H H1); cases (b2pT ? ? (orbP ? ?) H);
 189                 apply (p2bT ? ? (orbP ? ?));[left|right] assumption]]]]
 190 qed.
 191
 192 (* non mi e' chiaro a cosa serva ... *)
 193 lemma congr_S : ∀n,m.n = m → S n = S m.
 194 intros 1; cases n; intros; rewrite > H; reflexivity.
 195 qed.