Library Base
Global Set Implicit Arguments.
Global Unset Strict Implicit.
Require Export Omega List Morphisms.
Export ListNotations.
Ltac inv H := inversion H; subst; clear H.
Definition it X f n x := @nat_iter n X f x.
Definition id (X : Type) (x : X) := x.
Arguments id {X} x /.
Definition comp (X Y Z : Type) (f : Y -> Z) (g : X -> Y) : X -> Z :=
fun x => f (g x).
Notation "f 'o' g" := (comp f g) (at level 50).
Arguments comp {X Y Z} f g x /.
Definition dec (X : Prop) : Type := {X} + {~ X}.
Definition decision (X : Prop) (D : dec X) : dec X := D.
Arguments decision X {D}.
Existing Class dec.
Hint Unfold dec.
Notation "'eq_dec' X" := (forall x y : X, dec (x=y)) (at level 70).
Tactic Notation "decide" constr(p) :=
destruct (decision p).
Tactic Notation "decide" constr(p) "as" simple_intropattern(i) :=
destruct (decision p) as i.
Tactic Notation "decide" "claim" :=
match goal with
| |- dec (?p) => exact (decision p)
end.
Hint Extern 4 =>
match goal with
| [ |- dec ((fun _ => _) _) ] => simpl
end : typeclass_instances.
Instance eq_nat_Dec : eq_dec nat := eq_nat_dec.
Instance eq_list_dec X :
eq_dec X -> eq_dec (list X).
Proof.
intros D. apply list_eq_dec. exact D.
Defined.
Instance le_Dec (x y : nat) : dec (x <= y) := le_dec x y.
Instance True_dec : dec True := left I.
Instance False_dec : dec False := right (fun A => A).
Instance impl_dec (X Y : Prop) :
dec X -> dec Y -> dec (X -> Y).
Proof.
unfold dec ; tauto.
Qed.
Instance and_dec (X Y : Prop) : dec X -> dec Y -> dec (X /\ Y).
Proof.
unfold dec ; tauto.
Qed.
Instance or_dec (X Y : Prop) : dec X -> dec Y -> dec (X \/ Y).
Proof.
unfold dec ; tauto.
Qed.
Instance not_dec (X : Prop) : dec X -> dec (~ X).
Proof.
intros D. exact (decision (X -> False)).
Qed.
Lemma dec_DN X :
dec X -> ~~ X -> X.
Proof. unfold dec ; tauto. Qed.
Lemma dec_DM_and X Y :
dec X -> dec Y -> ~ (X /\ Y) -> ~ X \/ ~ Y.
Proof. unfold dec ; tauto. Qed.
Lemma dec_DM_impl X Y :
dec X -> dec Y -> ~ (X -> Y) -> X /\ ~ Y.
Proof. unfold dec ; tauto. Qed.
Lemma dec_prop_iff (X Y : Prop) :
(X <-> Y) -> dec X -> dec Y.
Proof.
intros A [B|B].
- left. tauto.
- right. tauto.
Qed.