blob: 14707914293d59ec480102b8dff3bda91e617f76 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
Require Import
Bool ZArith BVList Logic.
Local Coercion is_true : bool >-> Sortclass.
Section ReflectFacts.
Infix "-->" := implb (at level 60, right associativity) : bool_scope.
Lemma reflect_iff : forall P b, reflect P b -> (P<->b=true).
Proof.
intros; destruct H; intuition.
discriminate H.
Qed.
Lemma iff_reflect : forall P b, (P<->b=true) -> reflect P b.
Proof.
intros.
destr_bool; constructor; try now apply H.
unfold not. intros. apply H in H0. destruct H. easy.
Qed.
Lemma reflect_dec : forall P b, reflect P b -> {P} + {~P}.
Proof. intros; destruct H; [now left | now right]. Qed.
Lemma implyP : forall (b1 b2: bool), reflect (b1 -> b2) (b1 --> b2).
Proof. intros; apply iff_reflect; split;
case_eq b1; case_eq b2; intros; try easy; try compute in *; now apply H1.
Qed.
Lemma iffP : forall (b1 b2: bool), reflect (b1 <-> b2) (eqb b1 b2).
Proof. intros; apply iff_reflect; split;
case_eq b1; case_eq b2; intros; try easy; try compute in *; now apply H1.
Qed.
Lemma implyP2 : forall (b1 b2 b3: bool), reflect (b1 -> b2 -> b3) (b1 --> b2 --> b3).
Proof. intros; apply iff_reflect; split;
case_eq b1; case_eq b2; intros; try easy; try compute in *; now apply H1.
Qed.
Lemma andP : forall (b1 b2: bool), reflect (b1 /\ b2) (b1 && b2).
Proof. intros; apply iff_reflect; split;
case_eq b1; case_eq b2; intros; try easy; try compute in *; now apply H1.
Qed.
Lemma orP : forall (b1 b2: bool), reflect (b1 \/ b2) (b1 || b2).
Proof. intros; apply iff_reflect; split;
case_eq b1; case_eq b2; intros; try easy; try compute in *.
destruct H1 as [H1a | H1b ]; easy. left. easy. left. easy.
right. easy.
Qed.
Lemma negP : forall (b: bool), reflect (~ b) (negb b).
Proof. intros; apply iff_reflect; split;
case_eq b; intros; try easy; try compute in *.
contradict H0. easy.
Qed.
Lemma eqP : forall (b1 b2: bool), reflect (b1 = b2) (Bool.eqb b1 b2).
Proof. intros; apply iff_reflect; split;
case_eq b1; case_eq b2; intros; try easy; try compute in *; now apply H1.
Qed.
Lemma FalseB : (false = true) <-> False.
Proof. split; auto. discriminate. Qed.
Lemma TrueB : (true = true) <-> True.
Proof. split; auto. Qed.
End ReflectFacts.
|
