diff options
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Datatypes.v | 2 | ||||
| -rw-r--r-- | theories/Init/Logic.v | 7 | ||||
| -rw-r--r-- | theories/Init/Specif.v | 11 | ||||
| -rw-r--r-- | theories/Init/Tactics.v | 7 | ||||
| -rw-r--r-- | theories/Init/_CoqProject | 2 |
5 files changed, 27 insertions, 2 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 11d80dbc3..41e1fea61 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -65,7 +65,7 @@ Infix "&&" := andb : bool_scope. Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true. Proof. - destruct a; destruct b; intros; split; try (reflexivity || discriminate). + destruct a, b; repeat split; assumption. Qed. Hint Resolve andb_prop: bool. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index f659c31f9..3eefe9a84 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -223,7 +223,7 @@ Proof. Qed. (** [(IF_then_else P Q R)], written [IF P then Q else R] denotes - either [P] and [Q], or [~P] and [Q] *) + either [P] and [Q], or [~P] and [R] *) Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R. @@ -609,6 +609,11 @@ Proof. destruct 1; auto. Qed. +Lemma inhabited_covariant (A B : Type) : (A -> B) -> inhabited A -> inhabited B. +Proof. + intros f [x];exact (inhabits (f x)). +Qed. + (** Declaration of stepl and stepr for eq and iff *) Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 2cc2ecbc2..43a441fc5 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -207,6 +207,17 @@ Definition sig2_eta {A P Q} (p : { a : A | P a & Q a }) : p = exist2 _ _ (proj1_sig (sig_of_sig2 p)) (proj2_sig (sig_of_sig2 p)) (proj3_sig p). Proof. destruct p; reflexivity. Defined. +(** [exists x : A, B] is equivalent to [inhabited {x : A | B}] *) +Lemma exists_to_inhabited_sig {A P} : (exists x : A, P x) -> inhabited {x : A | P x}. +Proof. + intros [x y]. exact (inhabits (exist _ x y)). +Qed. + +Lemma inhabited_sig_to_exists {A P} : inhabited {x : A | P x} -> exists x : A, P x. +Proof. + intros [[x y]];exists x;exact y. +Qed. + (** [sumbool] is a boolean type equipped with the justification of their value *) diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 5d1e87ae0..7a846cd1b 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -236,3 +236,10 @@ Tactic Notation "clear" "dependent" hyp(h) := Tactic Notation "revert" "dependent" hyp(h) := generalize dependent h. + +(** Provide an error message for dependent induction that reports an import is +required to use it. Importing Coq.Program.Equality will shadow this notation +with the actual [dependent induction] tactic. *) + +Tactic Notation "dependent" "induction" ident(H) := + fail "To use dependent induction, first [Require Import Coq.Program.Equality.]". diff --git a/theories/Init/_CoqProject b/theories/Init/_CoqProject new file mode 100644 index 000000000..bff79d34b --- /dev/null +++ b/theories/Init/_CoqProject @@ -0,0 +1,2 @@ +-R .. Coq +-arg -noinit |