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 (* ### standard connectives/relations with reflection predicate ### *)
  60
  61 definition negb : bool → bool ≝ λb.match b with [ true ⇒ false | false ⇒ true].
  62
  63 lemma negbP : ∀b:bool.reflect (b = false) (negb b).
  64 intros (b); cases b; simplify; [apply reflect_false | apply reflect_true]
  65 [unfold Not; intros (H); destruct H | reflexivity]
  66 qed.
  67
  68 definition andb : bool → bool → bool ≝
  69   λa,b:bool. match a with [ true ⇒ b | false ⇒ false ].
  70
  71 lemma andbP : ∀a,b:bool. reflect (a = true ∧ b = true) (andb a b).
  72 intros (a b);
  73 generalize in match (refl_eq ? (andb a b));
  74 generalize in match (andb a b) in ⊢ (? ? ? % → %); intros 1 (c);
  75 cases c; intros (H); [ apply reflect_true | apply reflect_false ];
  76 generalize in match H; clear H;
  77 cases a; simplify;
  78 [1: intros (E); rewrite > E; split; reflexivity
  79 |2: intros (ABS); destruct ABS
  80 |3: intros (E); rewrite > E; unfold Not; intros (ABS); decompose;  destruct H1
  81 |4: intros (E); unfold Not; intros (ABS); decompose; destruct H]
  82 qed.
  83
  84 lemma andbPF : ∀a,b:bool. reflect (a = false ∨ b = false) (negb (andb a b)).
  85 intros (a b); cases a; cases b; simplify;
  86 [1: apply reflect_false | *: apply reflect_true ]
  87 [unfold Not; intros (H); cases H; destruct H1|right|left|left] reflexivity;
  88 qed.
  89
  90 definition orb : bool → bool → bool ≝
  91   λa,b.match a in bool with [true ⇒ true | false ⇒ b].
  92
  93 lemma orbP : ∀a,b:bool. reflect (a = true ∨ b = true) (orb a b).
  94 intros (a b); cases a; cases b; simplify;
  95 [1,2,3: apply reflect_true; [1,2: left | right ]; reflexivity
  96 | apply reflect_false; unfold Not; intros (H); cases H (E E); destruct E]
  97 qed.
  98
  99 lemma orbC : ∀a,b. orb a b = orb b a.
 100 intros (a b); cases a; cases b; auto. qed.
 101
 102 lemma lebP: ∀x,y. reflect (x ≤ y) (leb x y).
 103 intros (x y); generalize in match (leb_to_Prop x y);
 104 cases (leb x y); simplify; intros (H);
 105 [apply reflect_true | apply reflect_false ] assumption.
 106 qed.
 107
 108 lemma leb_refl : ∀n.leb n n = true.
 109 intros (n); apply (p2bT ? ? (lebP ? ?)); apply le_n; qed.
 110
 111 lemma lebW : ∀n,m. leb (S n) m = true → leb n m = true.
 112 intros (n m H); lapply (b2pT ? ? (lebP ? ?) H); clear H;
 113 apply (p2bT ? ? (lebP ? ?)); auto.
 114 qed.
 115
 116 definition ltb ≝ λx,y.leb (S x) y.
 117
 118 lemma ltbP: ∀x,y. reflect (x < y) (ltb x y).
 119 intros (x y); apply (lebP (S x) y);
 120 qed.
 121
 122 lemma ltb_refl : ∀n.ltb n n = false.
 123 intros (n); apply (p2bF ? ? (ltbP ? ?)); auto;
 124 qed.
 125
 126 (* ### = between booleans as <-> in Prop ### *)
 127 lemma eq_to_bool :
 128   ∀a,b:bool. a = b → (a = true → b = true) ∧ (b = true → a = true).
 129 intros (a b Eab); split; rewrite > Eab; intros; assumption;
 130 qed.
 131
 132 lemma bool_to_eq :
 133   ∀a,b:bool. (a = true → b = true) ∧ (b = true → a = true) → a = b.
 134 intros (a b Eab); decompose;
 135 generalize in match H; generalize in match H1; clear H; clear H1;
 136 cases a; cases b; intros (H1 H2);
 137 [2: rewrite > (H2 ?) | 3: rewrite > (H1 ?)] reflexivity;
 138 qed.
 139
 140
 141 lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m.
 142 intros (n m); apply bool_to_eq; split; intros (H);
 143 [1:cases (b2pT ? ? (orbP ? ?) H); [2: auto]
 144    rewrite > (eqb_true_to_eq ? ? H1); auto
 145 |2:cases (b2pT ? ? (lebP ? ?) H);
 146    [ elim n; [reflexivity|assumption]
 147    | simplify; rewrite > (p2bT ? ? (lebP ? ?) H1); rewrite > orbC ]
 148    reflexivity]
 149 qed.
 150
 151
 152 (* OUT OF PLACE *)
 153 lemma ltW : ∀n,m. n < m → n < (S m). intros; auto. 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.