Library CFML.Shared
Set Implicit Arguments.
Treatment of partially-applied equality
Require Import LibTactics LibCore LibEpsilon.
Hint Unfold pred_incl.
Tactic Notation "false" "~" constr(E) :=
false E; instantiate; auto_tilde.
Ltac app_evar t A cont ::=
let x := fresh "X" in
evar (x:A);
let t' := constr:(t x) in
let t'' := (eval unfold x in t') in
subst x; cont t''.
Treatment of partially-applied equality
Lemma if_eq_1 : forall A (x:bool) (v1 v2 y : A),
((if x then = v1 else = v2) y) -> (y = (if x then v1 else v2)).
Proof. tautob. Qed.
Lemma if_eq_2 : forall A (x:bool) (v1 v2 y : A),
((if x then eq v1 else = v2) y) -> (y = (if x then v1 else v2)).
Proof. tautob. Qed.
Lemma if_eq_3 : forall A (x:bool) (v1 v2 y : A),
((if x then = v1 else eq v2) y) -> (y = (if x then v1 else v2)).
Proof. tautob. Qed.
Lemma if_eq_4 : forall A (x:bool) (v1 v2 y : A),
((if x then eq v1 else eq v2) y) -> (y = (if x then v1 else v2)).
Proof. tautob. Qed.
Tactic Notation "if_eq" "in" hyp(H) :=
let go L := apply L in H in
first [ go if_eq_1 | go if_eq_2 | go if_eq_3 | go if_eq_4 ].
Tactic Notation "if_eq" :=
repeat match goal with H: ((if _ then _ else _) _) |- _ => if_eq in H end.
Ltac calc_partial_eq tt :=
repeat match goal with
| H: (= _) _ |- _ => simpl in H
| H: ((if _ then _ else _) _) |- _ => if_eq in H
end.
Ltac substs_core :=
let go x y := first [ subst x | subst y ] in
match goal with
| H: ?x = ?y |- _ => go x y
| H: (= ?x) ?y |- _ => simpl in H; go x y
end.
Ltac injects_core :=
match goal with
| H: ?f _ = ?f _ |- _ => injects H
| H: ?f _ _ = ?f _ _ |- _ => injects H
| H: ?f _ _ _ = ?f _ _ _ |- _ => injects H
| H: ?f _ _ _ _ = ?f _ _ _ _ |- _ => injects H
end.
Ltac substs_base :=
try rew_bool_eq in *; calc_partial_eq tt; repeat substs_core;
try injects_core;
try injects_core;
try injects_core;
try injects_core;
try injects_core.
Tactic Notation "substs" := substs_base.
Tactic Notation "substs" constr(z) :=
match goal with
| H: z = _ |- _ => subst z
| H: (= _) z |- _ => hnf in H; subst z
end.
Ltac subst_hyp_core H :=
match type of H with
| ?x = ?y => first [ subst x | subst y ]
end.
Lemma istrue_isTrue_forw : forall (P:Prop),
istrue (isTrue P) -> P.
Proof using. intros. rew_istrue~ in *. Qed.
Lemma eq_true_r_back : forall (b:bool),
b -> b = true.
Proof using. tautob. Qed.
Lemma eq_false_r_back : forall (b:bool),
!b -> b = false.
Proof using. tautob. Qed.
Ltac subst_hyp_base H :=
match type of H with
| ?x = ?y => first [ subst x | subst y ]
| istrue (isTrue (?x = ?y)) => apply istrue_isTrue_forw in H; first [ subst x | subst y ]
| istrue ?b => apply eq_true_r_back in H; subst_hyp_core H
| istrue (! ?b) => apply eq_false_r_back in H; subst_hyp_core H
end.
Tactic Notation "subst_hyp" hyp(H) :=
subst_hyp_base H.
Lemma demo_subst_hyp_2 : forall (x y : bool),
x -> !y -> x <> y.
Proof. introv H1 H2. subst_hyp H1. subst_hyp H2. auto. Qed.
Ltac apply_to_If cont :=
match goal with
| |- context [If ?B then _ else _] => cont B
| K: context [If ?B then _ else _] |- _ => cont B
end.
Ltac case_If_core B I1 I2:=
let H1 := fresh "TEMP" in let H2 := fresh "TEMP" in
destruct (classicT B) as [H1|H2];
[ tryfalse; rew_logic in H1; revert H1; intros I1; tryfalse
| tryfalse; rew_logic in H2; revert H2; intros I2; tryfalse ].
Tactic Notation "case_If" "as" simple_intropattern(I1) simple_intropattern(I2) :=
apply_to_If ltac:(fun B => case_If_core B I1 I2).
Tactic Notation "case_If" "as" simple_intropattern(I) :=
apply_to_If ltac:(fun B => case_If_core B I I).
Tactic Notation "case_If" :=
let C := fresh "C" in case_If as C.
Tag for preventing reductions
Definition blocker_def (A:Type) (X:A) : { Y:A | Y = X }.
Proof. constructors. eauto. Qed.
Definition blocker (A:Type) (X:A) := proj1_sig (blocker_def X).
Arguments blocker [A].
Definition blocker_eq : forall (A:Type) (X:A), blocker X = X.
Proof. intros. unfold blocker. apply (proj2_sig (blocker_def X)). Qed.
Ltac unblock_base C :=
match goal with |- context [ blocker (?U) ] =>
match U with
| C ?X1 => idtac
| C ?X1 ?X2 => idtac
| C ?X1 ?X2 ?X3 => idtac
| C ?X1 ?X2 ?X3 ?X4 => idtac
| C ?X1 ?X2 ?X3 ?X4 ?X5 => idtac
| C ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 => idtac
end;
replace (blocker U) with U ; [ | instantiate; rewrite blocker_eq; auto ]
end.
Tactic Notation "unblock" constr(C) :=
unblock_base C.
Tactic Notation "unblock" :=
repeat rewrite blocker_eq.
Notation "'%' X" := (@blocker _ X) (at level 1) : blocker_scope.
Open Scope blocker_scope.
Definition bool_of (P:Prop) :=
fun b => ((istrue b) = P).
Require Import LibEpsilon.
Section BoolOf.
Variables (b:bool) (P:Prop).
Lemma bool_of_true : bool_of P b -> b -> P.
Proof. unfold bool_of. intros. subst~. Qed.
Lemma bool_of_false : bool_of P b -> !b -> ~ P.
Proof. unfold bool_of. intros. subst~. destruct~ b. Qed.
Lemma bool_of_true_back : b -> bool_of P b -> P.
Proof. unfold bool_of. intros. subst~. Qed.
Lemma bool_of_false_back : !b -> bool_of P b -> ~ P.
Proof. unfold bool_of. intros. subst~. destruct~ b. Qed.
Lemma bool_of_true_in : bool_of P true -> P.
Proof. unfold bool_of. intros. subst~. Qed.
Lemma bool_of_false_in : bool_of P false -> ~ P.
Proof. unfold bool_of. intros. subst~. Qed.
Lemma bool_of_true_in_forw : P -> bool_of P true.
Proof. intros. hnf. extens*. Qed.
Lemma bool_of_false_in_forw : ~ P -> bool_of P false.
Proof. intros. hnf. extens; auto_false*. Qed.
Lemma bool_of_True : bool_of P b -> P -> b.
Proof. unfold bool_of. intros. subst~. Qed.
Lemma bool_of_False : bool_of P b -> ~ P -> !b.
Proof. unfold bool_of. intros. subst~. rew_istrue~. Qed.
Lemma bool_of_prove : (b <-> P) -> bool_of P b.
Proof. intros. unfold bool_of. extens*. Qed.
End BoolOf.
Lemma bool_of_eq : forall (P Q : Prop),
(P <-> Q) -> ((bool_of P) = (bool_of Q)).
Proof.
intros. extens. intros_all. unfold bool_of;
iff; rewrite H0; apply* prop_ext.
Qed.
Lemma elim_istrue_true : forall (b:bool) (P:Prop),
b -> (istrue b = P) -> P.
Proof. intros. subst~. Qed.
Lemma elim_istrue_false : forall (b:bool) (P:Prop),
!b -> (istrue b = P) -> ~ P.
Proof. intros_all. subst~. destruct b; simpls; false. Qed.
Lemma bool_of_impl : forall (P Q : Prop) x,
bool_of P x -> (P <-> Q) -> bool_of Q x.
Proof. unfold bool_of. intros. subst. extens*. Qed.
Lemma bool_of_impl_neg : forall (P Q : Prop) x,
bool_of P x -> (~P <-> Q) -> bool_of Q (!x).
Proof. unfold bool_of. intros. subst. extens. rew_istrue~. Qed.
Lemma bool_of_neg_impl : forall (P Q : Prop) x,
bool_of P (!x) -> (~P <-> Q) -> bool_of Q x.
Proof.
unfold bool_of. introv M K. subst. extens.
rew_istrue in K. rew_logic in K. auto.
Qed.
Lemma pred_le_bool_of : forall (P Q : Prop),
(P <-> Q) -> (pred_incl (bool_of P) (bool_of Q)).
Proof. unfold bool_of; intros_all. rewrite H0. apply~ prop_ext. Qed.
Tactics for normalizing hypotheses
Lemma true_eq_P : forall (P:Prop),
(istrue true = P) = P.
Proof. intros. apply prop_ext. iff. subst~. apply* prop_ext. Qed.
Hint Rewrite true_eq_P : rew_reflect.
Ltac fix_bool_of_known tt :=
match goal with
| H: bool_of ?P true |- _ =>
applys_to H bool_of_true_in
| H: bool_of ?P false |- _ =>
applys_to H bool_of_false_in
| H: bool_of ?P ?b, Hb: isTrue ?b |- _ =>
applys_to H (@bool_of_true_back b P Hb); clear Hb
| H: bool_of ?P ?b, Hb: isTrue (! ?b) |- _ =>
applys_to H (@bool_of_false_back b P Hb); clear Hb
| |- bool_of ?P true =>
apply bool_of_true_in_forw
| |- bool_of ?P false =>
apply bool_of_false_in_forw
| |- bool_of ?P ?b =>
first [ apply refl_equal
| apply bool_of_prove;
try (check_noevar_goal; rew_istrue) ]
end.
Tactic Notation "boolof" := fix_bool_of_known tt.
Tactic Notation "boolofs" := subst; fix_bool_of_known tt.
Tactic Notation "boolof" "*" := boolof; auto_star.
Tactic Notation "boolofs" "*" := boolofs; auto_star.
reflect_clean tt normalizes partially-applied equality
and calls the tactic rew_bool_eq, which normalizes bool/prop
coercions.
Ltac reflect_clean tt :=
calc_partial_eq tt; rew_bool_eq in *.
Ltac invert_first_hyp :=
let H := get_last_hyp tt in inverts H.
Ltac invert_first_hyp ::=
let H := get_last_hyp tt in symmetry in H; inverts H.
Notation "P ==> Q" := (pred_incl P Q)
(at level 55, right associativity) : func.
Open Scope func.
Hint Resolve pred_incl_refl.
Lemma weaken_bool_of : forall (P Q : Prop),
(P <-> Q) -> ((bool_of P) ==> (bool_of Q)).
Proof. unfold bool_of. intros_all. rewrite H0. extens*. Qed.
Definition rel_incl' A B (P Q:A->B->Prop) :=
forall r, (P r ==> Q r).
Notation "P ===> Q" := (rel_incl' P Q)
(at level 55, right associativity) : func.
Lemma refl_rel_incl' : forall A B (P:A->B->Prop),
P ===> P.
Proof using. apply refl_rel_incl. Qed.
Hint Resolve refl_rel_incl'.
Open Scope func.
Lemma pred_incl_extens : forall A (H1 H2 : A->Prop),
H1 ==> H2 -> H2 ==> H1 -> H1 = H2.
Proof. intros. extens*. Qed.
Lemma pred_incl_proj1 : forall A (H1 H2 : A->Prop),
H1 = H2 -> H1 ==> H2.
Proof. intros. subst~. Qed.
Lemma pred_incl_proj2 : forall A (H1 H2 : A->Prop),
H1 = H2 -> H2 ==> H1.
Proof. intros. subst~. Qed.
Arguments pred_incl_proj1 [A] [H1] [H2].
Arguments pred_incl_proj2 [A] [H1] [H2].
Arguments pred_incl_extens [A] [H1] [H2].
Hint Constructors mem.
Lemma not_True_to_False : ~ True -> False.
Proof. intros. rew_logic in *. auto. Qed.
Hint Immediate not_True_to_False.
Hint Resolve (0%nat) : typeclass_instances.
Hint Resolve (0%Z) : typeclass_instances.
Hint Resolve @nil : typeclass_instances.
Hint Resolve true : typeclass_instances.
Hint Resolve @None : typeclass_instances.
Hint Resolve @pair : typeclass_instances.
Lemma Inhab_intro : forall (A:Type),
A -> Inhab A.
Proof. introv x. apply (Inhab_of_val x). Qed.
Ltac inhab :=
intros; apply Inhab_intro; intros; try solve
[ eauto 10 with typeclass_instances
| constructor; eauto 10 with typeclass_instances
| apply arbitrary
| apply @arbitrary; eauto 10 with typeclass_instances ].
Instance Z_inhab : Inhab Z.
Proof. apply (Inhab_of_val 0%Z). Qed.
Hint Resolve Inhab_bool.
Lemma inhab_demo : Inhab Z.
Proof. inhab. Qed.
Hint Rewrite downto_eq upto_eq : rew_maths.
Hint Resolve wf_nat_upto : wf.
Hack for Zsub to be opaque. Use "Import ZsubNoSimpl."
to prevent unwanted simplifications of "-", while still
allowing "omega" tactic to work.