blob: bcfa4be367c05983080c4f077d0a0ee32b77a64d (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: IfProp.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
Require Bool.
Inductive IfProp [A,B:Prop] : bool-> Prop
:= Iftrue : A -> (IfProp A B true)
| Iffalse : B -> (IfProp A B false).
Hints Resolve Iftrue Iffalse : bool v62.
Lemma Iftrue_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=true -> A.
NewDestruct 1; Intros; Auto with bool.
Case diff_true_false; Auto with bool.
Qed.
Lemma Iffalse_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=false -> B.
NewDestruct 1; Intros; Auto with bool.
Case diff_true_false; Trivial with bool.
Qed.
Lemma IfProp_true : (A,B:Prop)(IfProp A B true) -> A.
Intros.
Inversion H.
Assumption.
Qed.
Lemma IfProp_false : (A,B:Prop)(IfProp A B false) -> B.
Intros.
Inversion H.
Assumption.
Qed.
Lemma IfProp_or : (A,B:Prop)(b:bool)(IfProp A B b) -> A\/B.
NewDestruct 1; Auto with bool.
Qed.
Lemma IfProp_sum : (A,B:Prop)(b:bool)(IfProp A B b) -> {A}+{B}.
NewDestruct b; Intro H.
Left; Inversion H; Auto with bool.
Right; Inversion H; Auto with bool.
Qed.
|
