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