This file collects a number of basic lemmas and tactics for better
proof automation, structuring large proofs, or rewriting. Most of
the rewriting support is ported from ss-reflect.
Symbols starting with vlib__ are internal.
Require Import Logic.Eqdep.
Require Import Bool.
Require Import Arith.
Require Import ZArith.
Require Import String.
Open Scope bool_scope.
Open Scope list_scope.
Set Implicit Arguments.
Unset Strict Implicit.
Require ClassicalFacts.
Require Export FunctionalExtensionality.
Require Export ProofIrrelevance.
Ltac exten := apply functional_extensionality.
Coersion of bool into Prop
Coersion of bools into Prop
Hints for auto
Lemma vlib__true_is_true : true.
Proof. reflexivity. Qed.
Lemma vlib__not_false_is_true : ~ false.
Proof. discriminate. Qed.
Hint Resolve vlib__true_is_true vlib__not_false_is_true.
Proof. reflexivity. Qed.
Lemma vlib__not_false_is_true : ~ false.
Proof. discriminate. Qed.
Hint Resolve vlib__true_is_true vlib__not_false_is_true.
Set up for basic simplification
Create HintDb vlib discriminated.
Adaptation of the ss-reflect "done" tactic.
Ltac vlib__basic_done :=
solve [trivial with vlib | apply sym_equal; trivial | discriminate | contradiction].
Ltac done := trivial with vlib; hnf; intros;
solve [try vlib__basic_done; split;
try vlib__basic_done; split;
try vlib__basic_done; split;
try vlib__basic_done; split;
try vlib__basic_done; split; vlib__basic_done
| match goal with H : ~ _ |- _ => solve [case H; trivial] end].
A variant of the ssr "done" tactic that performs "eassumption".
Ltac edone := try eassumption; trivial; hnf; intros;
solve [try eassumption; try vlib__basic_done; split;
try eassumption; try vlib__basic_done; split;
try eassumption; try vlib__basic_done; split;
try eassumption; try vlib__basic_done; split;
try eassumption; try vlib__basic_done; split;
try eassumption; vlib__basic_done
| match goal with H : ~ _ |- _ => solve [case H; trivial] end].
Tactic Notation "by" tactic(tac) := (tac; done).
Tactic Notation "eby" tactic(tac) := (tac; edone).
These definitions are ported from ssr-bool.
Negation lemmas
Section NegationLemmas.
Variables (b c : bool).
Lemma negbT : b = false -> negb b.
Proof. by case b. Qed.
Lemma negbTE: negb b -> b = false.
Proof. by case b. Qed.
Lemma negbF : b -> negb b = false.
Proof. by case b. Qed.
Lemma negbFE: negb b = false -> b.
Proof. by case b. Qed.
Lemma negbNE: negb (negb b) -> b.
Proof. by case b. Qed.
Lemma negbLR : b = negb c -> negb b = c.
Proof. by case c; intro X; rewrite X. Qed.
Lemma negbRL : negb b = c -> b = negb c.
Proof. by case b; intro X; rewrite <- X. Qed.
Lemma contra : (c -> b) -> negb b -> negb c.
Proof. by case b; case c. Qed.
End NegationLemmas.
Variables (b c : bool).
Lemma negbT : b = false -> negb b.
Proof. by case b. Qed.
Lemma negbTE: negb b -> b = false.
Proof. by case b. Qed.
Lemma negbF : b -> negb b = false.
Proof. by case b. Qed.
Lemma negbFE: negb b = false -> b.
Proof. by case b. Qed.
Lemma negbNE: negb (negb b) -> b.
Proof. by case b. Qed.
Lemma negbLR : b = negb c -> negb b = c.
Proof. by case c; intro X; rewrite X. Qed.
Lemma negbRL : negb b = c -> b = negb c.
Proof. by case b; intro X; rewrite <- X. Qed.
Lemma contra : (c -> b) -> negb b -> negb c.
Proof. by case b; case c. Qed.
End NegationLemmas.
Lemmas for ifs, which allow reasoning about the condition without
repeating it inside the proof.
Section BoolIf.
Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A).
Inductive if_spec : A -> bool -> Set :=
| IfSpecTrue : b -> if_spec vT true
| IfSpecFalse : b = false -> if_spec vF false.
Lemma ifP : if_spec (if b then vT else vF) b.
Proof. by case_eq b; constructor. Qed.
Lemma if_same : (if b then vT else vT) = vT.
Proof. by case b. Qed.
Lemma if_neg : (if negb b then vT else vF) = if b then vF else vT.
Proof. by case b. Qed.
Lemma fun_if : f (if b then vT else vF) = if b then f vT else f vF.
Proof. by case b. Qed.
Lemma if_arg : forall fT fF : A -> B,
(if b then fT else fF) x = if b then fT x else fF x.
Proof. by case b. Qed.
End BoolIf.
Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A).
Inductive if_spec : A -> bool -> Set :=
| IfSpecTrue : b -> if_spec vT true
| IfSpecFalse : b = false -> if_spec vF false.
Lemma ifP : if_spec (if b then vT else vF) b.
Proof. by case_eq b; constructor. Qed.
Lemma if_same : (if b then vT else vT) = vT.
Proof. by case b. Qed.
Lemma if_neg : (if negb b then vT else vF) = if b then vF else vT.
Proof. by case b. Qed.
Lemma fun_if : f (if b then vT else vF) = if b then f vT else f vF.
Proof. by case b. Qed.
Lemma if_arg : forall fT fF : A -> B,
(if b then fT else fF) x = if b then fT x else fF x.
Proof. by case b. Qed.
End BoolIf.
The reflection predicate
Inductive reflect (P : Prop) : bool -> Set :=
| ReflectT : P -> reflect P true
| ReflectF : ~ P -> reflect P false.
| ReflectT : P -> reflect P true
| ReflectF : ~ P -> reflect P false.
Internal reflection lemmas
Section ReflectCore.
Variables (P : Prop) (b : bool) (Hb : reflect P b) (Q : Prop) (c : bool).
Lemma introNTF : (if c then ~ P else P) -> negb b = c.
Proof. by case c; case Hb. Qed.
Lemma introTF : (if c then P else ~ P) -> b = c.
Proof. by case c; case Hb. Qed.
Lemma elimNTF : negb b = c -> if c then ~ P else P.
Proof. by intro X; rewrite <- X; case Hb. Qed.
Lemma elimTF : b = c -> if c then P else ~ P.
Proof. by intro X; rewrite <- X; case Hb. Qed.
Lemma equivPif : (Q -> P) -> (P -> Q) -> if b then Q else ~ Q.
Proof. by case Hb; auto. Qed.
Lemma xorPif : Q \/ P -> ~ (Q /\ P) -> if b then ~ Q else Q.
Proof. by case Hb; [intros ? _ H ? | intros ? H _]; case H. Qed.
End ReflectCore.
Variables (P : Prop) (b : bool) (Hb : reflect P b) (Q : Prop) (c : bool).
Lemma introNTF : (if c then ~ P else P) -> negb b = c.
Proof. by case c; case Hb. Qed.
Lemma introTF : (if c then P else ~ P) -> b = c.
Proof. by case c; case Hb. Qed.
Lemma elimNTF : negb b = c -> if c then ~ P else P.
Proof. by intro X; rewrite <- X; case Hb. Qed.
Lemma elimTF : b = c -> if c then P else ~ P.
Proof. by intro X; rewrite <- X; case Hb. Qed.
Lemma equivPif : (Q -> P) -> (P -> Q) -> if b then Q else ~ Q.
Proof. by case Hb; auto. Qed.
Lemma xorPif : Q \/ P -> ~ (Q /\ P) -> if b then ~ Q else Q.
Proof. by case Hb; [intros ? _ H ? | intros ? H _]; case H. Qed.
End ReflectCore.
Internal negated reflection lemmas
Section ReflectNegCore.
Variables (P : Prop) (b : bool) (Hb : reflect P (negb b)) (Q : Prop) (c : bool).
Lemma introTFn : (if c then ~ P else P) -> b = c.
Proof. by intro X; apply (introNTF Hb) in X; rewrite <- X; case b. Qed.
Lemma elimTFn : b = c -> if c then ~ P else P.
Proof. by intro X; rewrite <- X; apply (elimNTF Hb); case b. Qed.
Lemma equivPifn : (Q -> P) -> (P -> Q) -> if b then ~ Q else Q.
Proof. by rewrite <- if_neg; apply equivPif. Qed.
Lemma xorPifn : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q.
Proof. by rewrite <- if_neg; apply xorPif. Qed.
End ReflectNegCore.
Variables (P : Prop) (b : bool) (Hb : reflect P (negb b)) (Q : Prop) (c : bool).
Lemma introTFn : (if c then ~ P else P) -> b = c.
Proof. by intro X; apply (introNTF Hb) in X; rewrite <- X; case b. Qed.
Lemma elimTFn : b = c -> if c then ~ P else P.
Proof. by intro X; rewrite <- X; apply (elimNTF Hb); case b. Qed.
Lemma equivPifn : (Q -> P) -> (P -> Q) -> if b then ~ Q else Q.
Proof. by rewrite <- if_neg; apply equivPif. Qed.
Lemma xorPifn : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q.
Proof. by rewrite <- if_neg; apply xorPif. Qed.
End ReflectNegCore.
User-oriented reflection lemmas
Section Reflect.
Variables (P Q : Prop) (b b' c : bool).
Hypotheses (Pb : reflect P b) (Pb' : reflect P (negb b')).
Lemma introT : P -> b.
Proof. by apply (introTF Pb (c:=true)). Qed.
Lemma introF : ~ P -> b = false.
Proof. by apply (introTF Pb (c:=false)). Qed.
Lemma introN : ~ P -> negb b.
Proof. by apply (introNTF Pb (c:=true)). Qed.
Lemma introNf : P -> negb b = false.
Proof. by apply (introNTF Pb (c:=false)). Qed.
Lemma introTn : ~ P -> b'.
Proof. by apply (introTFn Pb' (c:=true)). Qed.
Lemma introFn : P -> b' = false.
Proof. by apply (introTFn Pb' (c:=false)). Qed.
Lemma elimT : b -> P.
Proof. by apply (@elimTF _ _ Pb true). Qed.
Lemma elimF : b = false -> ~ P.
Proof. by apply (@elimTF _ _ Pb false). Qed.
Lemma elimN : negb b -> ~P.
Proof. by apply (@elimNTF _ _ Pb true). Qed.
Lemma elimNf : negb b = false -> P.
Proof. by apply (@elimNTF _ _ Pb false). Qed.
Lemma elimTn : b' -> ~ P.
Proof. by apply (@elimTFn _ _ Pb' true). Qed.
Lemma elimFn : b' = false -> P.
Proof. by apply (@elimTFn _ _ Pb' false). Qed.
Lemma introP : (b -> Q) -> (negb b -> ~ Q) -> reflect Q b.
Proof. by case b; constructor; auto. Qed.
Lemma iffP : (P -> Q) -> (Q -> P) -> reflect Q b.
Proof. by case Pb; constructor; auto. Qed.
Lemma appP : reflect Q b -> P -> Q.
Proof. by intro Qb; intro X; apply introT in X; revert X; case Qb. Qed.
Lemma sameP : reflect P c -> b = c.
Proof. intro X; case X; [exact introT | exact introF]. Qed.
Lemma decPcases : if b then P else ~ P.
Proof. by case Pb. Qed.
Definition decP : {P} + {~ P}.
Proof. by generalize decPcases; case b; [left | right]. Defined.
End Reflect.
Coercion elimT : reflect >-> Funclass.
Section ReflectConnectives.
Variable b1 b2 b3 b4 b5 : bool.
Lemma idP : reflect b1 b1.
Proof. by case b1; constructor. Qed.
Lemma idPn : reflect (negb b1) (negb b1).
Proof. by case b1; constructor. Qed.
Lemma negP : reflect (~ b1) (negb b1).
Proof. by case b1; constructor; auto. Qed.
Lemma negPn : reflect b1 (negb (negb b1)).
Proof. by case b1; constructor. Qed.
Lemma negPf : reflect (b1 = false) (negb b1).
Proof. by case b1; constructor. Qed.
Lemma andP : reflect (b1 /\ b2) (b1 && b2).
Proof. by case b1; case b2; constructor; try done; intro X; case X. Qed.
Lemma orP : reflect (b1 \/ b2) (b1 || b2).
Proof. by case b1; case b2; constructor; auto; intro X; case X. Qed.
Lemma nandP : reflect (negb b1 \/ negb b2) (negb (b1 && b2)).
Proof. by case b1; case b2; constructor; auto; intro X; case X; auto. Qed.
Lemma norP : reflect (negb b1 /\ negb b2) (negb (b1 || b2)).
Proof. by case b1; case b2; constructor; auto; intro X; case X; auto. Qed.
End ReflectConnectives.
Variables (P Q : Prop) (b b' c : bool).
Hypotheses (Pb : reflect P b) (Pb' : reflect P (negb b')).
Lemma introT : P -> b.
Proof. by apply (introTF Pb (c:=true)). Qed.
Lemma introF : ~ P -> b = false.
Proof. by apply (introTF Pb (c:=false)). Qed.
Lemma introN : ~ P -> negb b.
Proof. by apply (introNTF Pb (c:=true)). Qed.
Lemma introNf : P -> negb b = false.
Proof. by apply (introNTF Pb (c:=false)). Qed.
Lemma introTn : ~ P -> b'.
Proof. by apply (introTFn Pb' (c:=true)). Qed.
Lemma introFn : P -> b' = false.
Proof. by apply (introTFn Pb' (c:=false)). Qed.
Lemma elimT : b -> P.
Proof. by apply (@elimTF _ _ Pb true). Qed.
Lemma elimF : b = false -> ~ P.
Proof. by apply (@elimTF _ _ Pb false). Qed.
Lemma elimN : negb b -> ~P.
Proof. by apply (@elimNTF _ _ Pb true). Qed.
Lemma elimNf : negb b = false -> P.
Proof. by apply (@elimNTF _ _ Pb false). Qed.
Lemma elimTn : b' -> ~ P.
Proof. by apply (@elimTFn _ _ Pb' true). Qed.
Lemma elimFn : b' = false -> P.
Proof. by apply (@elimTFn _ _ Pb' false). Qed.
Lemma introP : (b -> Q) -> (negb b -> ~ Q) -> reflect Q b.
Proof. by case b; constructor; auto. Qed.
Lemma iffP : (P -> Q) -> (Q -> P) -> reflect Q b.
Proof. by case Pb; constructor; auto. Qed.
Lemma appP : reflect Q b -> P -> Q.
Proof. by intro Qb; intro X; apply introT in X; revert X; case Qb. Qed.
Lemma sameP : reflect P c -> b = c.
Proof. intro X; case X; [exact introT | exact introF]. Qed.
Lemma decPcases : if b then P else ~ P.
Proof. by case Pb. Qed.
Definition decP : {P} + {~ P}.
Proof. by generalize decPcases; case b; [left | right]. Defined.
End Reflect.
Coercion elimT : reflect >-> Funclass.
Section ReflectConnectives.
Variable b1 b2 b3 b4 b5 : bool.
Lemma idP : reflect b1 b1.
Proof. by case b1; constructor. Qed.
Lemma idPn : reflect (negb b1) (negb b1).
Proof. by case b1; constructor. Qed.
Lemma negP : reflect (~ b1) (negb b1).
Proof. by case b1; constructor; auto. Qed.
Lemma negPn : reflect b1 (negb (negb b1)).
Proof. by case b1; constructor. Qed.
Lemma negPf : reflect (b1 = false) (negb b1).
Proof. by case b1; constructor. Qed.
Lemma andP : reflect (b1 /\ b2) (b1 && b2).
Proof. by case b1; case b2; constructor; try done; intro X; case X. Qed.
Lemma orP : reflect (b1 \/ b2) (b1 || b2).
Proof. by case b1; case b2; constructor; auto; intro X; case X. Qed.
Lemma nandP : reflect (negb b1 \/ negb b2) (negb (b1 && b2)).
Proof. by case b1; case b2; constructor; auto; intro X; case X; auto. Qed.
Lemma norP : reflect (negb b1 /\ negb b2) (negb (b1 || b2)).
Proof. by case b1; case b2; constructor; auto; intro X; case X; auto. Qed.
End ReflectConnectives.
These definitions are ported from ssr-eq.
Inductive phantom (T : Type) (p : T) : Type := Phantom.
Implicit Arguments phantom [].
Implicit Arguments Phantom [].
Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2.
Definition idfun T := (fun x : T => x).
Module Equality.
Definition axiom T (e : T -> T -> bool) := forall x y, reflect (x = y) (e x y).
Structure mixin_of T := Mixin {op : T -> T -> bool; _ : axiom op}.
Notation class_of := mixin_of (only parsing).
Section ClassDef.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (T : Type) (cT : type).
Definition class cT' := match cT' return class_of cT' with Pack _ c _ => c end.
Definition pack c := @Pack T c T.
Definition clone := fun c (_ : cT -> T) (_ : phant_id (pack c) cT) => pack c.
End ClassDef.
Module Exports.
Coercion sort : type >-> Sortclass.
Notation eqType := type.
Notation EqMixin := Mixin.
Notation EqType T m := (@pack T m).
Notation "[ 'eqMixin' 'of' T ]" := (class _ : mixin_of T)
(at level 0, format "[ 'eqMixin' 'of' T ]") : form_scope.
Notation "[ 'eqType' 'of' T 'for' C ]" := (@clone T C _ idfun id)
(at level 0, format "[ 'eqType' 'of' T 'for' C ]") : form_scope.
Notation "[ 'eqType' 'of' T ]" := (@clone T _ _ id id)
(at level 0, format "[ 'eqType' 'of' T ]") : form_scope.
End Exports.
End Equality.
Export Equality.Exports.
Definition eq_op T := Equality.op (Equality.class T).
Implicit Arguments eq_op [[T]].
Lemma eqE : forall T x, eq_op x = Equality.op (Equality.class T) x.
Proof. done. Qed.
Lemma eqP : forall T, Equality.axiom (@eq_op T).
Proof. by unfold eq_op; destruct T as (? & []). Qed.
Implicit Arguments eqP [T].
Notation "x == y" := (eq_op x y)
(at level 70, no associativity) : bool_scope.
Notation "x == y :> T" := ((x : T) == (y : T))
(at level 70, y at next level) : bool_scope.
Notation "x != y" := (negb (x == y))
(at level 70, no associativity) : bool_scope.
Notation "x != y :> T" := (negb (x == y :> T))
(at level 70, y at next level) : bool_scope.
Lemma vlib__internal_eqP :
forall (T: eqType) (x y : T), reflect (x = y) (x == y).
Proof. apply eqP. Qed.
Lemma neqP : forall (T: eqType) (x y: T), reflect (x <> y) (x != y).
Proof. intros; case eqP; constructor; auto. Qed.
Lemma beq_refl : forall (T : eqType) (x : T), x == x.
Proof. by intros; case eqP. Qed.
Lemma beq_sym : forall (T : eqType) (x y : T), (x == y) = (y == x).
Proof. intros; do 2 case eqP; congruence. Qed.
Hint Resolve beq_refl : vlib.
Hint Rewrite beq_refl : vlib_trivial.
Notation eqxx := beq_refl.
Lemma vlib__negb_rewrite : forall b, negb b -> b = false.
Proof. by intros []. Qed.
Lemma vlib__andb_split : forall b1 b2, b1 && b2 -> b1 /\ b2.
Proof. by intros [] []. Qed.
Lemma vlib__nandb_split : forall b1 b2, b1 && b2 = false -> b1 = false \/ b2 = false.
Proof. intros [] []; auto. Qed.
Lemma vlib__orb_split : forall b1 b2, b1 || b2 -> b1 \/ b2.
Proof. intros [] []; auto. Qed.
Lemma vlib__norb_split : forall b1 b2, b1 || b2 = false -> b1 = false /\ b2 = false.
Proof. intros [] []; auto. Qed.
Lemma vlib__eqb_split : forall b1 b2 : bool, (b1 -> b2) -> (b2 -> b1) -> b1 = b2.
Proof. intros [] [] H H'; unfold is_true in *; auto using sym_eq. Qed.
Lemma vlib__beq_rewrite : forall (T : eqType) (x1 x2 : T), x1 == x2 -> x1 = x2.
Proof. by intros until 0; case eqP. Qed.
Set up for basic simplification: database of reflection lemmas
Create HintDb vlib_refl discriminated.
Hint Resolve andP orP nandP norP negP vlib__internal_eqP neqP : vlib_refl.
Ltac vlib__complaining_inj f H :=
let X := fresh in
(match goal with | [|- ?P ] => set (X := P) end);
injection H;
clear H; intros; subst X;
try subst.
Ltac vlib__clarify1 :=
try subst;
repeat match goal with
| [H: is_true (andb _ _) |- _] =>
let H' := fresh H in case (vlib__andb_split H); clear H; intros H' H
| [H: is_true (negb ?x) |- _] => rewrite (vlib__negb_rewrite H) in *
| [H: is_true ?x |- _] => rewrite H in *
| [H: ?x = true |- _] => rewrite H in *
| [H: ?x = false |- _] => rewrite H in *
| [H: is_true (_ == _) |- _] => generalize (vlib__beq_rewrite H); clear H; intro H
| [H: @existT _ _ _ _ = @existT _ _ _ _ |- _] => apply inj_pair2 in H; try subst
| [H: ?f _ = ?f _ |- _] => vlib__complaining_inj f H
| [H: ?f _ _ = ?f _ _ |- _] => vlib__complaining_inj f H
| [H: ?f _ _ _ = ?f _ _ _ |- _] => vlib__complaining_inj f H
| [H: ?f _ _ _ _ = ?f _ _ _ _ |- _] => vlib__complaining_inj f H
| [H: ?f _ _ _ _ _ = ?f _ _ _ _ _ |- _] => vlib__complaining_inj f H
| [H: ?f _ _ _ _ _ _ = ?f _ _ _ _ _ _ |- _] => vlib__complaining_inj f H
| [H: ?f _ _ _ _ _ _ _ = ?f _ _ _ _ _ _ _ |- _] => vlib__complaining_inj f H
end; try done.
Perform injections & discriminations on all hypotheses
Ltac clarify :=
vlib__clarify1;
repeat match goal with
| H1: ?x = Some _, H2: ?x = None |- _ => rewrite H2 in H1; discriminate
| H1: ?x = Some _, H2: ?x = Some _ |- _ => rewrite H2 in H1; vlib__clarify1
end; try done.
Kill simple goals that require up to two econstructor calls.
Ltac vauto :=
(clarify; try edone;
try (econstructor (solve [edone | econstructor (edone) ]))).
Check that the hypothesis id is defined. This is useful to make sure that
an assert has been completely finished.
Ltac end_assert id :=
let m := fresh in
pose (m := refl_equal id); clear m.
Ltac inv x := inversion x; clarify.
Ltac simpls := simpl in *; try done.
Ltac ins := simpl in *; try done; intros.
Tactic Notation "case_eq" constr(x) := case_eq (x).
Tactic Notation "case_eq" constr(x) "as" simple_intropattern(H) :=
destruct x as [] _eqn: H; try done.
Ltac vlib__clarsimp1 :=
clarify; (autorewrite with vlib_trivial vlib in * );
(autorewrite with vlib_trivial in * ); try done;
clarify; auto 1 with vlib.
Ltac clarsimp := intros; simpl in *; vlib__clarsimp1.
Ltac autos := clarsimp; auto with vlib.
Destruct but give useful names
Definition NW (P: unit -> Prop) : Prop := P tt.
Notation "<< x : t >>" := (NW (fun x => t)) (at level 80, x ident, no associativity).
Notation "<< t >>" := (NW (fun _ => t)) (at level 79, no associativity).
Ltac unnw := unfold NW in *.
Ltac rednw := red; unnw.
Hint Unfold NW.
Destruct, but no case split
Ltac desc :=
repeat match goal with
| H: is_true (_ == _) |- _ => generalize (vlib__beq_rewrite H); clear H; intro H
| H : exists x, NW (fun y => _) |- _ =>
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : exists x, ?p |- _ =>
let x' := fresh x in destruct H as [x' H]
| H : ?p /\ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => red in x' | _ => idtac end;
match q with | NW _ => red in y' | _ => idtac end
| H : is_true (_ && _) |- _ =>
let H' := fresh H in case (vlib__andb_split H); clear H; intros H H'
| H : (_ || _) = false |- _ =>
let H' := fresh H in case (vlib__norb_split H); clear H; intros H H'
| H : ?x = ?x |- _ => clear H
end.
Ltac des :=
repeat match goal with
| H: is_true (_ == _) |- _ => generalize (vlib__beq_rewrite H); clear H; intro H
| H : exists x, NW (fun y => _) |- _ =>
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : exists x, ?p |- _ =>
let x' := fresh x in destruct H as [x' H]
| H : ?p /\ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => red in x' | _ => idtac end;
match q with | NW _ => red in y' | _ => idtac end
| H : is_true (_ && _) |- _ =>
let H' := fresh H in case (vlib__andb_split H); clear H; intros H H'
| H : (_ || _) = false |- _ =>
let H' := fresh H in case (vlib__norb_split H); clear H; intros H H'
| H : ?x = ?x |- _ => clear H
| H : ?p <-> ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => unfold NW at 1 in x'; red in y' | _ => idtac end;
match q with | NW _ => unfold NW at 1 in y'; red in x' | _ => idtac end
| H : ?p \/ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => H end in
destruct H as [x' | y'];
[ match p with | NW _ => red in x' | _ => idtac end
| match q with | NW _ => red in y' | _ => idtac end]
| H : is_true (_ || _) |- _ => case (vlib__orb_split H); clear H; intro H
| H : (_ && _) = false |- _ => case (vlib__nandb_split H); clear H; intro H
end.
Ltac des_if :=
clarify;
repeat
match goal with
| |- context[match ?x with _ => _ end] =>
match (type of x) with
| { _ } + { _ } => destruct x; clarify
| bool =>
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with vlib_refl);
subst P; destruct Heq as [Heq|Heq]
| _ => let Heq := fresh "Heq" in destruct x as [] _eqn: Heq; clarify
end
| H: context[ match ?x with _ => _ end ] |- _ =>
match (type of x) with
| { _ } + { _ } => destruct x; clarify
| bool =>
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with vlib_refl);
subst P; destruct Heq as [Heq|Heq]
| _ => let Heq := fresh "Heq" in destruct x as [] _eqn: Heq; clarify
end
end.
Ltac des_eqrefl :=
match goal with
| H: context[match ?X as id return (id = ?X -> _) with _ => _ end Logic.eq_refl] |- _ =>
let EQ := fresh "EQ" in
let id' := fresh "x" in
revert H;
generalize (Logic.eq_refl X); generalize X at 1 3;
intros id' EQ; destruct id'; intros H
| |- context[match ?X as id return (id = ?X -> _) with _ => _ end Logic.eq_refl] =>
let EQ := fresh "EQ" in
let id' := fresh "x" in
generalize (Logic.eq_refl X); generalize X at 1 3;
intros id' EQ; destruct id'
end.
Ltac desf := clarify; des; des_if.
Ltac clarassoc := clarsimp; autorewrite with vlib_trivial vlib vlibA in *; try done.
Ltac vlib__hacksimp1 :=
clarsimp;
match goal with
| H: _ |- _ => solve [rewrite H; clear H; clarsimp
|rewrite <- H; clear H; clarsimp]
| _ => solve [f_equal; clarsimp]
end.
Ltac hacksimp :=
clarsimp;
try match goal with
| H: _ |- _ => solve [rewrite H; clear H; clarsimp
|rewrite <- H; clear H; clarsimp]
| |- context[match ?p with _ => _ end] => solve [destruct p; vlib__hacksimp1]
| _ => solve [f_equal; clarsimp]
end.
repeat match goal with
| H: is_true (_ == _) |- _ => generalize (vlib__beq_rewrite H); clear H; intro H
| H : exists x, NW (fun y => _) |- _ =>
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : exists x, ?p |- _ =>
let x' := fresh x in destruct H as [x' H]
| H : ?p /\ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => red in x' | _ => idtac end;
match q with | NW _ => red in y' | _ => idtac end
| H : is_true (_ && _) |- _ =>
let H' := fresh H in case (vlib__andb_split H); clear H; intros H H'
| H : (_ || _) = false |- _ =>
let H' := fresh H in case (vlib__norb_split H); clear H; intros H H'
| H : ?x = ?x |- _ => clear H
end.
Ltac des :=
repeat match goal with
| H: is_true (_ == _) |- _ => generalize (vlib__beq_rewrite H); clear H; intro H
| H : exists x, NW (fun y => _) |- _ =>
let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
| H : exists x, ?p |- _ =>
let x' := fresh x in destruct H as [x' H]
| H : ?p /\ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => red in x' | _ => idtac end;
match q with | NW _ => red in y' | _ => idtac end
| H : is_true (_ && _) |- _ =>
let H' := fresh H in case (vlib__andb_split H); clear H; intros H H'
| H : (_ || _) = false |- _ =>
let H' := fresh H in case (vlib__norb_split H); clear H; intros H H'
| H : ?x = ?x |- _ => clear H
| H : ?p <-> ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => fresh H end in
destruct H as [x' y'];
match p with | NW _ => unfold NW at 1 in x'; red in y' | _ => idtac end;
match q with | NW _ => unfold NW at 1 in y'; red in x' | _ => idtac end
| H : ?p \/ ?q |- _ =>
let x' := match p with | NW (fun z => _) => fresh z | _ => H end in
let y' := match q with | NW (fun z => _) => fresh z | _ => H end in
destruct H as [x' | y'];
[ match p with | NW _ => red in x' | _ => idtac end
| match q with | NW _ => red in y' | _ => idtac end]
| H : is_true (_ || _) |- _ => case (vlib__orb_split H); clear H; intro H
| H : (_ && _) = false |- _ => case (vlib__nandb_split H); clear H; intro H
end.
Ltac des_if :=
clarify;
repeat
match goal with
| |- context[match ?x with _ => _ end] =>
match (type of x) with
| { _ } + { _ } => destruct x; clarify
| bool =>
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with vlib_refl);
subst P; destruct Heq as [Heq|Heq]
| _ => let Heq := fresh "Heq" in destruct x as [] _eqn: Heq; clarify
end
| H: context[ match ?x with _ => _ end ] |- _ =>
match (type of x) with
| { _ } + { _ } => destruct x; clarify
| bool =>
let Heq := fresh "Heq" in
let P := fresh in
evar(P: Prop);
assert (Heq: reflect P x) by (subst P; trivial with vlib_refl);
subst P; destruct Heq as [Heq|Heq]
| _ => let Heq := fresh "Heq" in destruct x as [] _eqn: Heq; clarify
end
end.
Ltac des_eqrefl :=
match goal with
| H: context[match ?X as id return (id = ?X -> _) with _ => _ end Logic.eq_refl] |- _ =>
let EQ := fresh "EQ" in
let id' := fresh "x" in
revert H;
generalize (Logic.eq_refl X); generalize X at 1 3;
intros id' EQ; destruct id'; intros H
| |- context[match ?X as id return (id = ?X -> _) with _ => _ end Logic.eq_refl] =>
let EQ := fresh "EQ" in
let id' := fresh "x" in
generalize (Logic.eq_refl X); generalize X at 1 3;
intros id' EQ; destruct id'
end.
Ltac desf := clarify; des; des_if.
Ltac clarassoc := clarsimp; autorewrite with vlib_trivial vlib vlibA in *; try done.
Ltac vlib__hacksimp1 :=
clarsimp;
match goal with
| H: _ |- _ => solve [rewrite H; clear H; clarsimp
|rewrite <- H; clear H; clarsimp]
| _ => solve [f_equal; clarsimp]
end.
Ltac hacksimp :=
clarsimp;
try match goal with
| H: _ |- _ => solve [rewrite H; clear H; clarsimp
|rewrite <- H; clear H; clarsimp]
| |- context[match ?p with _ => _ end] => solve [destruct p; vlib__hacksimp1]
| _ => solve [f_equal; clarsimp]
end.
Named case tactics (taken from Libtactics)
Tactic Notation "assert_eq" ident(x) constr(v) :=
let H := fresh in
assert (x = v) as H by reflexivity;
clear H.
Tactic Notation "Case_aux" ident(x) constr(name) :=
first [
set (x := name); move x at top
| assert_eq x name
| fail 1 "because we are working on a different case." ].
Ltac Case name := Case_aux case name.
Ltac SCase name := Case_aux subcase name.
Ltac SSCase name := Case_aux subsubcase name.
Ltac SSSCase name := Case_aux subsubsubcase name.
Ltac SSSSCase name := Case_aux subsubsubsubcase name.
Lightweight case tactics (without names)
Tactic Notation "--" tactic(c) :=
first [
assert (WithinCaseM := True); move WithinCaseM at top
| fail 1 "because we are working on a different case." ]; c.
Tactic Notation "++" tactic(c) :=
first [
assert (WithinCaseP := True); move WithinCaseP at top
| fail 1 "because we are working on a different case." ]; c.
Exploit an assumption (adapted from CompCert).
Ltac exploit x :=
refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _ _) _)
|| refine ((fun x y => y x) (x _ _ _) _)
|| refine ((fun x y => y x) (x _ _) _)
|| refine ((fun x y => y x) (x _) _).
Tactic Notation "induction" "[" ident_list(y) "]" ident(x) :=
first [ try (intros until x); revert y; induction x
| red; try (intros until x); revert y; induction x ].
Tactic Notation "induction" "[" ident_list(y) "]" ident(x) "[" ident(z) "]" :=
first [ try (intros until x); revert y; induction x; destruct z
| red; try (intros until x); revert y; induction x; destruct z ].
Tactic Notation "induction" "[" ident_list(y) "]" ident(x) "[" ident(z) ident (w) "]" :=
first [ try (intros until x); revert y; induction x; destruct z, w
| red; try (intros until x); revert y; induction x; destruct z, w ].
Versions with hacksimp
Tactic Notation "induct" ident(x) := induction x; hacksimp.
Tactic Notation "induct" ident(x) "[" ident(z) "]" :=
induction x; destruct z; hacksimp.
Tactic Notation "induct" ident(x) "[" ident(z) ident(w) "]" :=
induction x; destruct z, w; hacksimp.
Tactic Notation "induct" "[" ident_list(y) "]" ident(x) :=
first [ try (intros until x); revert y; induction x; hacksimp
| red; try (intros until x); revert y; induction x; hacksimp ].
Tactic Notation "induct" "[" ident_list(y) "]" ident(x) "[" ident(z) "]" :=
first [ try (intros until x); revert y; induction x; destruct z; hacksimp
| red; try (intros until x); revert y; induction x; destruct z; hacksimp ].
Tactic Notation "induct" "[" ident_list(y) "]" ident(x) "[" ident(z) ident(w) "]" :=
first [ try (intros until x); revert y; induction x; destruct z, w; hacksimp
| red; try (intros until x); revert y; induction x; destruct z, w; hacksimp ].
Ltac vlib__apply_refl :=
intros;
match goal with
| |- is_true ?p => eapply introT; [solve [trivial with vlib_refl]|]
| |- ?p = true => eapply introT; [solve [trivial with vlib_refl]|]
| |- ?p = false => eapply introFn; [solve [trivial with vlib_refl]|]
| |- ?p = false => eapply introF; [solve [trivial with vlib_refl]|]
| |- _ => red; vlib__apply_refl
end.
Tactic Notation "apply" "/" := vlib__apply_refl.
Tactic Notation "apply" "/" constr(X) :=
first [eapply X | eapply elimT; [eapply X; edone|]
| eapply introT; [eapply X; edone|]
| eapply introFn; [eapply X; edone|]
| eapply introF; [eapply X; edone|]].
Tactic Notation "split" "/" :=
first [split | hnf; intros; apply/ ; split
| try red; intros; apply vlib__eqb_split].
apply in assumption
Ltac vlib__apply_refl_in H :=
first [eapply elimT in H; [|solve [trivial with vlib_refl]]
|eapply elimFn in H; [|solve [trivial with vlib_refl]]
|eapply elimF in H; [|solve [trivial with vlib_refl]]].
Ltac vlib__apply_with_in X H :=
first [eapply X in H
|eapply elimT in H; [|eapply X; edone]
|eapply elimFn in H; [|eapply X; edone]
|eapply elimF in H; [|eapply X; edone]].
Tactic Notation "apply" "/" "in" hyp(H) := vlib__apply_refl_in H.
Tactic Notation "apply" "/" constr(X) "in" hyp(H) := vlib__apply_with_in X H.
move (apply to top of goal)
Ltac vlib__move_refl := let top := fresh in intro top; vlib__apply_refl_in top; revert top.
Ltac vlib__move_with X := let top := fresh in intro top; vlib__apply_with_in X top; revert top.
Tactic Notation "move" "=>" simple_intropattern_list(L)
:= intros L.
Tactic Notation "move" ":" ident_list(Y)
:= revert Y.
Tactic Notation "move" ":" ident_list(Y) "=>" simple_intropattern_list(L)
:= revert Y; intros L.
Tactic Notation "move" "/"
:= vlib__move_refl.
Tactic Notation "move" "/" ":" ident_list(Y)
:= revert Y; vlib__move_refl.
Tactic Notation "move" "/" "=>" simple_intropattern_list(L)
:= vlib__move_refl; intros L.
Tactic Notation "move" "/" ":" ident_list(Y) "=>" simple_intropattern_list(L)
:= revert Y; vlib__move_refl; intros L.
Tactic Notation "move" "/" constr(X) ident_list(Y)
:= revert Y; vlib__move_with X.
Tactic Notation "move" "/" constr(X) ident_list(Y) "=>" simple_intropattern_list(L)
:= revert Y; vlib__move_with X; intros L.
Tactic Notation "move" "/" constr(X) ":" ident_list(Y)
:= revert Y; vlib__move_with X.
Tactic Notation "move" "/" constr(X) ":" ident_list(Y) "=>" simple_intropattern_list(L)
:= revert Y; vlib__move_with X; intros L.
case
Ltac vlib__case_plain
:= let top := fresh in intro top; case top; clear top.
Ltac vlib__case_refl
:= let top := fresh in intro top; vlib__apply_refl_in top; case top; clear top.
Ltac vlib__case_with X
:= let top := fresh in intro top; vlib__apply_with_in X top; case top; clear top.
Tactic Notation "case" "=>" simple_intropattern_list(L)
:= vlib__case_plain; intros L.
Tactic Notation "case" ":" ident_list(Y)
:= revert Y; vlib__case_plain.
Tactic Notation "case" ":" ident_list(Y) "=>" simple_intropattern_list(L)
:= revert Y; vlib__case_plain; intros L.
Tactic Notation "case" "/"
:= vlib__case_refl.
Tactic Notation "case" "/" ":" ident_list(Y)
:= revert Y; vlib__case_refl.
Tactic Notation "case" "/" "=>" simple_intropattern_list(L)
:= vlib__case_refl; intros L.
Tactic Notation "case" "/" ":" ident_list(Y) "=>" simple_intropattern_list(L)
:= revert Y; vlib__case_refl; intros L.
Tactic Notation "case" "/" constr(X) ident_list(Y)
:= revert Y; vlib__case_with X.
Tactic Notation "case" "/" constr(X) ident_list(Y) "=>" simple_intropattern_list(L)
:= revert Y; vlib__case_with X; intros L.
Tactic Notation "case" "/" constr(X) ":" ident_list(Y)
:= revert Y; vlib__case_with X.
Tactic Notation "case" "/" constr(X) ":" ident_list(Y) "=>" simple_intropattern_list(L)
:= revert Y; vlib__case_with X; intros L.
double apply
Tactic Notation "apply" "/" constr(X1) "/" constr(X2) :=
eapply sameP; [apply X1; edone|eapply iffP; [apply X2; edone|instantiate|instantiate]].
Delimit Scope fun_scope with FUN.
Open Scope fun_scope.
Notation "f ^~ y" := (fun x => f x y)
(at level 10, y at level 8, no associativity, format "f ^~ y") : fun_scope.
Module Option.
Definition apply aT rT (f : aT -> rT) x u :=
match u with
| Some y => f y
| None => x
end.
Definition default T := apply (fun x : T => x).
Definition bind aT rT (f : aT -> option rT) := apply f None.
Definition map aT rT (f : aT -> rT) := bind (fun x => Some (f x)).
End Option.
Notation oapp := Option.apply.
Notation odflt := Option.default.
Notation obind := Option.bind.
Notation omap := Option.map.
Notation some := (@Some _) (only parsing).
Definitions and notation for explicit functions with simplification.
Section SimplFun.
Variables aT rT : Type.
Inductive simpl_fun : Type := SimplFun (_ : aT -> rT).
Definition fun_of_simpl := fun f x => match f with SimplFun lam => lam x end.
Coercion fun_of_simpl : simpl_fun >-> Funclass.
End SimplFun.
Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E))
(at level 0,
format "'[hv' [ 'fun' : T => '/ ' E ] ']'") : fun_scope.
Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E))
(at level 0, x ident,
format "'[hv' [ 'fun' x => '/ ' E ] ']'") : fun_scope.
Notation "[ 'fun' x : T => E ]" := (SimplFun (fun x : T => E))
(at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E])
(at level 0, x ident, y ident,
format "'[hv' [ 'fun' x y => '/ ' E ] ']'") : fun_scope.
Notation "[ 'fun' x y : T => E ]" := (fun x : T => [fun y : T => E])
(at level 0, x ident, y ident, only parsing) : fun_scope.
Notation "[ 'fun' ( x : T ) y => E ]" := (fun x : T => [fun y => E])
(at level 0, x ident, y ident, only parsing) : fun_scope.
Notation "[ 'fun' x ( y : T ) => E ]" := (fun x => [fun y : T => E])
(at level 0, x ident, y ident, only parsing) : fun_scope.
Notation "[ 'fun' ( x : xT ) ( y : yT ) => E ]" :=
(fun x : xT => [fun y : yT => E])
(at level 0, x ident, y ident, only parsing) : fun_scope.
Definition erefl := @eq_refl.
Definition esym := eq_sym.
Definition nesym := sym_not_eq.
Definition etrans := eq_trans.
Definition congr1 := f_equal.
Definition congr2 := f_equal2.
A predicate for singleton types.
Definition all_equal_to T (x0 : T) := forall x, x = x0.
Lemma unitE : all_equal_to tt.
Proof. by intros []. Qed.
Lemma unitE : all_equal_to tt.
Proof. by intros []. Qed.
A generic wrapper type
Extensional equality for unary and binary functions + syntactic sugar.
Section ExtensionalEquality.
Variables A B C : Type.
Definition eqfun (f g : B -> A) : Prop := forall x, f x = g x.
Definition eqrel (r s : C -> B -> A) : Prop := forall x y, r x y = s x y.
Lemma frefl : forall f, eqfun f f.
Proof. done. Qed.
Lemma fsym : forall f g, eqfun f g -> eqfun g f.
Proof. red; done. Qed.
Lemma ftrans : forall f g h (EQ1: eqfun f g) (EQ2: eqfun g h), eqfun f h.
Proof. by red; intros; rewrite EQ1. Qed.
Lemma rrefl : forall r, eqrel r r.
Proof. done. Qed.
End ExtensionalEquality.
Hint Resolve frefl rrefl.
Notation "f1 =1 f2" := (eqfun f1 f2)
(at level 70, no associativity) : fun_scope.
Notation "f1 =1 f2 :> A" := (f1 =1 (f2 : A))
(at level 70, f2 at next level, A at level 90) : fun_scope.
Notation "f1 =2 f2" := (eqrel f1 f2)
(at level 70, no associativity) : fun_scope.
Notation "f1 =2 f2 :> A" := (f1 =2 (f2 : A))
(at level 70, f2 at next level, A, B at level 90) : fun_scope.
Section Composition.
Variables A B C : Type.
Definition funcomp u (f : B -> A) (g : C -> B) x := match u with tt => f (g x) end.
Local Notation comp := (funcomp tt).
Definition pcomp (f : B -> option A) (g : C -> option B) x := obind f (g x).
Lemma eq_comp : forall f f' g g', f =1 f' -> g =1 g' -> comp f g =1 comp f' g'.
Proof. red; intros; simpl; congruence. Qed.
End Composition.
Notation "[ 'eta' f ]" := (fun x => f x)
(at level 0, format "[ 'eta' f ]") : fun_scope.
Notation id := (fun x => x).
Notation "@ 'id' T " := (fun x : T => x)
(at level 10, T at level 8, only parsing) : fun_scope.
Notation comp := (funcomp tt).
Notation "@ 'comp'" := (fun A B C => @funcomp A B C tt).
Notation "f1 \o f2" := (comp f1 f2) (at level 50) : fun_scope.
Section Morphism.
Variables (aT rT sT : Type) (f : aT -> rT).
Definition morphism_1 aF rF := forall x, f (aF x) = rF (f x).
Definition morphism_2 aOp rOp := forall x y, f (aOp x y) = rOp (f x) (f y).
End Morphism.
Notation "{ 'morph' f : x / a >-> r }" :=
(morphism_1 f (fun x => a) (fun x => r))
(at level 0, f at level 99, x ident,
format "{ 'morph' f : x / a >-> r }") : type_scope.
Notation "{ 'morph' f : x / a }" :=
(morphism_1 f (fun x => a) (fun x => a))
(at level 0, f at level 99, x ident,
format "{ 'morph' f : x / a }") : type_scope.
Notation "{ 'morph' f : x y / a >-> r }" :=
(morphism_2 f (fun x y => a) (fun x y => r))
(at level 0, f at level 99, x ident, y ident,
format "{ 'morph' f : x y / a >-> r }") : type_scope.
Notation "{ 'morph' f : x y / a }" :=
(morphism_2 f (fun x y => a) (fun x y => a))
(at level 0, f at level 99, x ident, y ident,
format "{ 'morph' f : x y / a }") : type_scope.
Section Injections.
Variables (rT aT : Type) (f : aT -> rT).
Definition injective := forall x1 x2, f x1 = f x2 -> x1 = x2.
Definition cancel g := forall x, g (f x) = x.
Definition pcancel g := forall x, g (f x) = Some x.
Definition ocancel (g : aT -> option rT) h := forall x, oapp h x (g x) = x.
Lemma can_pcan : forall g, cancel g -> pcancel (fun y => Some (g y)).
Proof. by red; intros; f_equal. Qed.
Lemma pcan_inj : forall g, pcancel g -> injective.
Proof. red; intros; apply (congr1 g) in H0; rewrite !H in *; clarify. Qed.
Lemma can_inj : forall g, cancel g -> injective.
Proof. eby intros; apply can_pcan in H; eapply pcan_inj. Qed.
Lemma canLR : forall g x y, cancel g -> x = f y -> g x = y.
Proof. intros; clarify. Qed.
Lemma canRL : forall g x y, cancel g -> f x = y -> x = g y.
Proof. intros; clarify. Qed.
End Injections.
Lemma esymK : forall T x y, cancel (@eq_sym T x y) (@eq_sym T y x).
Proof. by red; destruct x0. Qed.
Lemma etrans_id : forall T x y (eqxy : x = y :> T),
eq_trans (eq_refl x) eqxy = eqxy.
Proof. by destruct eqxy. Qed.
Section InjectionsTheory.
Variables (A B C : Type) (f g : B -> A) (h : C -> B).
Lemma inj_id : injective (@id A).
Proof. done. Qed.
Lemma inj_can_sym : forall f', cancel f f' -> injective f' -> cancel f' f.
Proof. red; intros; apply H0, H. Qed.
Lemma inj_comp : injective f -> injective h -> injective (f \o h).
Proof. by red; simpl; intros; apply H0, H. Qed.
Lemma can_comp : forall f' h',
cancel f f' -> cancel h h' -> cancel (f \o h) (h' \o f').
Proof. by red; simpl; intros; rewrite H, H0. Qed.
Lemma pcan_pcomp : forall f' h',
pcancel f f' -> pcancel h h' -> pcancel (f \o h) (pcomp h' f').
Proof. by red; intros; unfold pcomp; simpl; rewrite H; simpl; rewrite H0. Qed.
Lemma eq_inj : injective f -> f =1 g -> injective g.
Proof. intros H H0 x y; simpl; rewrite <- !H0; apply H. Qed.
Lemma eq_can : forall f' g', cancel f f' -> f =1 g -> f' =1 g' -> cancel g g'.
Proof. by red; intros; rewrite <- H0, <- H1. Qed.
Lemma inj_can_eq : forall f',
cancel f f' -> injective f' -> cancel g f' -> f =1 g.
Proof. by red; intros; apply H0; rewrite H1. Qed.
End InjectionsTheory.
Section Bijections.
Variables (A B : Type) (f : B -> A).
Inductive bijective : Prop := Bijective g (_ : cancel f g) (_ : cancel g f).
Hypothesis bijf : bijective.
Lemma bij_inj : injective f.
Proof. eby destruct bijf; eapply can_inj. Qed.
Lemma bij_can_sym : forall f', cancel f' f <-> cancel f f'.
Proof.
split; intros; [by apply inj_can_sym, bij_inj|].
by destruct bijf; intros x; rewrite <- (H1 x), H.
Qed.
Lemma bij_can_eq : forall f' f'', cancel f f' -> cancel f f'' -> f' =1 f''.
Proof.
by intros; eapply inj_can_eq, bij_can_sym; [apply bij_can_sym | apply bij_inj |].
Qed.
End Bijections.
Section BijectionsTheory.
Variables (A B C : Type) (f : B -> A) (h : C -> B).
Lemma eq_bij : bijective f -> forall g, f =1 g -> bijective g.
Proof. by destruct 1; exists g; eapply eq_can; eauto. Qed.
Lemma bij_comp : bijective f -> bijective h -> bijective (f \o h).
Proof.
intros [f' fK f'K] [h' hK h'K].
by exists (h' \o f' : _ -> _); apply can_comp; auto.
Qed.
Lemma bij_can_bij : bijective f -> forall f', cancel f f' -> bijective f'.
Proof. by exists f; [apply (bij_can_sym H) |]. Qed.
End BijectionsTheory.
Section Involutions.
Variables (A : Type) (f : A -> A).
Definition involutive := cancel f f.
Hypothesis Hf : involutive.
Lemma inv_inj : injective f.
Proof. eapply can_inj, Hf. Qed.
Lemma inv_bij : bijective f.
Proof. by exists f. Qed.
End Involutions.
Section OperationProperties.
Variables S T R : Type.
Section SopTisR.
Implicit Type op : S -> T -> R.
Definition left_inverse e inv op := forall x, op (inv x) x = e.
Definition right_inverse e inv op := forall x, op x (inv x) = e.
End SopTisR.
Section SopTisS.
Implicit Type op : S -> T -> S.
Definition right_id e op := forall x, op x e = x.
Definition left_zero z op := forall x, op z x = z.
Definition right_commutative op := forall x y z, op (op x y) z = op (op x z) y.
Definition left_distributive op add :=
forall x y z, op (add x y) z = add (op x z) (op y z).
End SopTisS.
Section SopTisT.
Implicit Type op : S -> T -> T.
Definition left_id e op := forall x, op e x = x.
Definition right_zero z op := forall x, op x z = z.
Definition left_commutative op := forall x y z, op x (op y z) = op y (op x z).
Definition right_distributive op add :=
forall x y z, op x (add y z) = add (op x y) (op x z).
End SopTisT.
Section SopSisT.
Implicit Type op : S -> S -> T.
Definition self_inverse e op := forall x, op x x = e.
Definition commutative op := forall x y, op x y = op y x.
End SopSisT.
Section SopSisS.
Implicit Type op : S -> S -> S.
Definition idempotent op := forall x, op x x = x.
Definition associative op := forall x y z, op x (op y z) = op (op x y) z.
End SopSisS.
End OperationProperties.
Lemma andTb : forall x, true && x = x.
Proof. done. Qed.
Lemma andFb : forall x, false && x = false.
Proof. done. Qed.
Lemma andbT : forall x, x && true = x.
Proof. by intros []. Qed.
Lemma andbF : forall x, x && false = false.
Proof. by intros []. Qed.
Lemma andbb : forall x, x && x = x.
Proof. by intros []. Qed.
Lemma andbC : forall x y, x && y = y && x.
Proof. by intros[][]. Qed.
Lemma andbA : forall x y z, x && (y && z) = x && y && z.
Proof. by intros[][][]. Qed.
Lemma andbCA : forall x y z, x && (y && z) = y && (x && z).
Proof. by intros[][][]. Qed.
Lemma andbAC : forall x y z, x && y && z = x && z && y.
Proof. by intros[][][]. Qed.
Lemma andbN : forall b, b && negb b = false.
Proof. by intros[]. Qed.
Lemma andNb : forall b, negb b && b = false.
Proof. by intros[]. Qed.
Lemma orTb : forall x, true || x = true.
Proof. done. Qed.
Lemma orFb : forall x, false || x = x.
Proof. done. Qed.
Lemma orbT : forall x, x || true = true.
Proof. by intros[]. Qed.
Lemma orbF : forall x, x || false = x.
Proof. by intros[]. Qed.
Lemma orbb : forall x, x || x = x.
Proof. by intros[]. Qed.
Lemma orbC : forall x y, x || y = y || x.
Proof. by intros[][]. Qed.
Lemma orbA : forall x y z, x || (y || z) = x || y || z.
Proof. by intros[][][]. Qed.
Lemma orbCA : forall x y z, x || (y || z) = y || (x || z).
Proof. by intros[][][]. Qed.
Lemma orbAC : forall x y z, x || y || z = x || z || y.
Proof. by intros[][][]. Qed.
Lemma orbN : forall b, b || negb b = true.
Proof. by intros[]. Qed.
Lemma orNb : forall b, negb b || b = true.
Proof. by intros[]. Qed.
Lemma andb_orl : forall x y z, (x || y) && z = x && z || y && z.
Proof. by intros[][][]. Qed.
Lemma andb_orr : forall x y z, x && (y || z) = x && y || x && z.
Proof. by intros[][][]. Qed.
Lemma orb_andl : forall x y z, (x && y) || z = (x || z) && (y || z).
Proof. by intros[][][]. Qed.
Lemma orb_andr : forall x y z, x || (y && z) = (x || y) && (x || z).
Proof. by intros[][][]. Qed.
Pseudo-cancellation -- i.e, absorbtion
Lemma andbK : forall b1 b2, b1 && b2 || b1 = b1.
Proof. by intros[][]. Qed.
Lemma andKb : forall b1 b2, b1 || b2 && b1 = b1.
Proof. by intros[][]. Qed.
Lemma orbK : forall b1 b2, (b1 || b2) && b1 = b1.
Proof. by intros[][]. Qed.
Lemma orKb : forall b1 b2, b1 && (b2 || b1) = b1.
Proof. by intros[][]. Qed.
Exclusive or -- xorb
Lemma xorFb : forall x, xorb false x = x.
Proof. by intros[]. Qed.
Lemma xorbF : forall x, xorb x false = x.
Proof. by intros[]. Qed.
Lemma xorTb : forall x, xorb true x = negb x.
Proof. by intros[]. Qed.
Lemma xorbT : forall x, xorb x true = negb x.
Proof. by intros[]. Qed.
Lemma xorbb : forall x, xorb x x = false.
Proof. by intros[]. Qed.
Lemma xorbC : forall x y, xorb x y = xorb y x.
Proof. by intros[][]. Qed.
Lemma xorbA : forall x y z, xorb x (xorb y z) = xorb (xorb x y) z.
Proof. by intros[][][]. Qed.
Lemma xorbCA : forall x y z, xorb x (xorb y z) = xorb y (xorb x z).
Proof. by intros[][][]. Qed.
Lemma xorbAC : forall x y z, xorb (xorb x y) z = xorb (xorb x z) y.
Proof. by intros[][][]. Qed.
Lemma xorbN : forall x y, xorb x (negb y) = negb (xorb x y).
Proof. by intros[][]. Qed.
Lemma xorNb : forall x y, xorb x (negb y) = negb (xorb x y).
Proof. by intros[][]. Qed.
Lemma andb_xorl : forall x y z, (xorb x y) && z = xorb (x && z) (y && z).
Proof. by intros[][][]. Qed.
Lemma andb_xorr : forall x y z, x && (xorb y z) = xorb (x && y) (x && z).
Proof. by intros[][][]. Qed.
Negation
Lemma negb_neg : forall x, negb (negb x) = x.
Proof. by intros[]. Qed.
Lemma negb_and : forall x y, negb (x && y) = negb x || negb y.
Proof. by intros[][]. Qed.
Lemma negb_or : forall x y, negb (x || y) = negb x && negb y.
Proof. by intros[][]. Qed.
Lemma negb_xor : forall x y, negb (xorb x y) = xorb (negb x) y.
Proof. by intros[][]. Qed.
Hint Rewrite
andTb andFb andbT andbF
orTb orFb orbT orbF
: vlib_trivial.
Hint Rewrite
andbb andbN andNb
orbb orbN orNb
andbK andKb orbK orKb
xorbb xorFb xorbF xorTb xorbT xorbb negb_neg
: vlib.
Hint Rewrite andbA orbA xorbA : vlibA.
An attempt to replicate functionality from ss-reflect.
Section ApplyIff.
Variables P Q : Prop.
Hypothesis eqPQ : P <-> Q.
Lemma iffLR : P -> Q.
Proof. tauto. Qed.
Lemma iffRL : Q -> P.
Proof. tauto. Qed.
Lemma iffLRn : ~P -> ~Q.
Proof. tauto. Qed.
Lemma iffRLn : ~Q -> ~P.
Proof. tauto. Qed.
End ApplyIff.
Definition pred T := T -> bool.
Identity Coercion fun_of_pred : pred >-> Funclass.
Definition rel T := T -> pred T.
Identity Coercion fun_of_rel : rel >-> Funclass.
Notation xpred0 := (fun _ => false).
Notation xpredT := (fun _ => true).
Notation xpredI := (fun (p1 p2 : pred _) x => p1 x && p2 x).
Notation xpredU := (fun (p1 p2 : pred _) x => p1 x || p2 x).
Notation xpredC := (fun (p : pred _) x => negb (p x)).
Notation xpredD := (fun (p1 p2 : pred _) x => negb (p2 x) && p1 x).
Notation xpreim := (fun f (p : pred _) x => p (f x)).
Notation xrelU := (fun (r1 r2 : rel _) x y => r1 x y || r2 x y).
Section Predicates.
Variables T : Type.
Definition subpred (p1 p2 : pred T) := forall x, p1 x -> p2 x.
Definition subrel (r1 r2 : rel T) := forall x y, r1 x y -> r2 x y.
Definition simpl_pred := simpl_fun T bool.
Definition SimplPred (p : pred T) : simpl_pred := SimplFun p.
Coercion pred_of_simpl (p : simpl_pred) : pred T := p : T -> bool.
Definition pred0 := SimplPred xpred0.
Definition predT := SimplPred xpredT.
Definition predI p1 p2 := SimplPred (xpredI p1 p2).
Definition predU p1 p2 := SimplPred (xpredU p1 p2).
Definition predC p := SimplPred (xpredC p).
Definition predD p1 p2 := SimplPred (xpredD p1 p2).
Definition preim rT f (d : pred rT) := SimplPred (xpreim f d).
Definition simpl_rel := simpl_fun T (pred T).
Definition SimplRel (r : rel T) : simpl_rel := [fun x => r x].
Coercion rel_of_simpl_rel (r : simpl_rel) : rel T := fun x y => r x y.
Definition relU r1 r2 := SimplRel (xrelU r1 r2).
Lemma subrelUl : forall r1 r2, subrel r1 (relU r1 r2).
Proof. red; ins; apply/orP; vauto. Qed.
Lemma subrelUr : forall r1 r2, subrel r2 (relU r1 r2).
Proof. red; ins; apply/orP; vauto. Qed.
Inductive mem_pred : Type := Mem (_ : pred T).
Definition isMem pT topred mem :=
mem = (fun p : pT => Mem (fun x => topred p x)).
Structure predType : Type := PredType {
pred_sort :> Type;
topred : pred_sort -> pred T;
_ : {mem | isMem topred mem}
}.
Definition mkPredType pT toP := PredType (exist (@isMem pT toP) _ eq_refl).
Canonical Structure predPredType := Eval hnf in @mkPredType (pred T) id.
Canonical Structure simplPredType := Eval hnf in mkPredType pred_of_simpl.
Coercion pred_of_mem mp : pred_sort predPredType :=
match mp with Mem p => fun x => p x end.
Canonical Structure memPredType := Eval hnf in mkPredType pred_of_mem.
Definition clone_pred U :=
fun pT (_ : pred_sort pT -> U) =>
fun a mP (pT' := @PredType U a mP) (_ : phant_id pT' pT) => pT'.
End Predicates.
Implicit Arguments topred [[T] p].
Implicit Arguments pred0 [T].
Implicit Arguments predT [T].
Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E))
(at level 0, format "[ 'pred' : T | E ]") : fun_scope.
Notation "[ 'pred' x | E ]" := (SimplPred (fun x => E))
(at level 0, x ident, format "[ 'pred' x | E ]") : fun_scope.
Notation "[ 'pred' x : T | E ]" := (SimplPred (fun x : T => E))
(at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E))
(at level 0, x ident, y ident, format "[ 'rel' x y | E ]") : fun_scope.
Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E))
(at level 0, x ident, y ident, only parsing) : fun_scope.
Notation "[ 'predType' 'Of' T ]" := (@clone_pred _ T _ id _ _ id)
(at level 0, format "[ 'predType' 'Of' T ]") : form_scope.
Notation pred_class := (pred_sort (predPredType _)).
Coercion sort_of_simpl_pred T (p : simpl_pred T) : pred_class := p : pred T.
Definition predArgType := Type.
Identity Coercion sort_of_predArgType : predArgType >-> Sortclass.
Coercion pred_of_argType (T : predArgType) : simpl_pred T := predT.
Notation "{ : T }" := (T%type : predArgType)
(at level 0, format "{ : T }") : type_scope.
Definition mem T (pT : predType T) : pT -> mem_pred T :=
match tt with tt =>
(match pT return pT -> _ with PredType _ _ (exist mem _) => mem end)
end.
Definition in_mem T x mp :=
match tt with tt => @pred_of_mem T mp x end.
Implicit Arguments mem [[T] pT].
Coercion pred_of_mem_pred T mp := [pred x : T | in_mem x mp].
Definition eq_mem T p1 p2 := forall x : T, in_mem x p1 = in_mem x p2.
Definition sub_mem T p1 p2 := forall x : T, in_mem x p1 -> in_mem x p2.
Reserved Notation "x \in A" (at level 70, no associativity).
Reserved Notation "x \notin A" (at level 70, no associativity).
Reserved Notation "p1 =i p2" (at level 70, no associativity).
Notation "x \in A" := (in_mem x (mem A)) : bool_scope.
Notation "x \in A" := (in_mem x (mem A)) : bool_scope.
Notation "x \notin A" := (negb (x \in A)) : bool_scope.
Notation "A =i B" := (eq_mem (mem A) (mem B)) : type_scope.
Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B))
(at level 0, A, B at level 69,
format "{ '[hv' 'subset' A '/ ' <= B ']' }") : type_scope.
Notation "[ 'mem' A ]" := (pred_of_simpl (pred_of_mem_pred (mem A)))
(at level 0, only parsing) : fun_scope.
Notation "[ 'rel' 'Of' fA ]" := (fun x => [mem (fA x)])
(at level 0, format "[ 'rel' 'Of' fA ]") : fun_scope.
Notation "[ 'predI' A & B ]" := (predI [mem A] [mem B])
(at level 0, format "[ 'predI' A & B ]") : fun_scope.
Notation "[ 'predU' A & B ]" := (predU [mem A] [mem B])
(at level 0, format "[ 'predU' A & B ]") : fun_scope.
Notation "[ 'predD' A & B ]" := (predD [mem A] [mem B])
(at level 0, format "[ 'predD' A & B ]") : fun_scope.
Notation "[ 'predC' A ]" := (predC [mem A])
(at level 0, format "[ 'predC' A ]") : fun_scope.
Notation "[ 'preim' f 'Of' A ]" := (preim f [mem A])
(at level 0, format "[ 'preim' f 'Of' A ]") : fun_scope.
Notation "[ 'pred' x \in A ]" := [pred x | x \in A]
(at level 0, x ident, format "[ 'pred' x \in A ]") : fun_scope.
Notation "[ 'pred' x \in A | E ]" := [pred x | (x \in A) && E]
(at level 0, x ident, format "[ 'pred' x \in A | E ]") : fun_scope.
Notation "[ 'rel' x y \in A & B | E ]" :=
[rel x y | (x \in A) && (y \in B) && E]
(at level 0, x ident, y ident,
format "[ 'rel' x y \in A & B | E ]") : fun_scope.
Notation "[ 'rel' x y \in A & B ]" := [rel x y | (x \in A) && (y \in B)]
(at level 0, x ident, y ident,
format "[ 'rel' x y \in A & B ]") : fun_scope.
Notation "[ 'rel' x y \in A | E ]" := [rel x y \in A & A | E]
(at level 0, x ident, y ident,
format "[ 'rel' x y \in A | E ]") : fun_scope.
Notation "[ 'rel' x y \in A ]" := [rel x y \in A & A]
(at level 0, x ident, y ident,
format "[ 'rel' x y \in A ]") : fun_scope.
Section simpl_mem.
Variables (T : Type) (pT : predType T).
Lemma mem_topred : forall (p : pT), mem (topred p) = mem p.
Proof. by unfold mem; case pT; intros T1 app1 [mem1 ->]. Qed.
Lemma topredE : forall x (p : pT), topred p x = (x \in p).
Proof. by intros; rewrite <-mem_topred. Qed.
Lemma in_simpl : forall x (p : simpl_pred T), (x \in p) = p x.
Proof. done. Qed.
Lemma simpl_predE : forall (p : pred T), [pred x | p x] =1 p.
Proof. done. Qed.
Lemma mem_simpl : forall (p : simpl_pred T), mem p = p :> pred T.
Proof. done. Qed.
Definition memE := mem_simpl.
End simpl_mem.
Section RelationProperties.
Variable T : Type.
Variable R : rel T.
Definition total := forall x y, R x y || R y x.
Definition transitive := forall x y z, R x y -> R y z -> R x z.
Definition symmetric := forall x y, R x y = R y x.
Definition antisymmetric := forall x y, R x y -> R y x -> x = y.
Definition pre_symmetric := forall x y, R x y -> R y x.
Lemma symmetric_from_pre : pre_symmetric -> symmetric.
Proof. split/; apply H. Qed.
Lemma pre_from_symmetric : symmetric -> pre_symmetric.
Proof. by red; ins; rewrite H. Qed.
Definition reflexive := forall x, R x x.
Definition irreflexive := forall x, R x x = false.
Definition left_transitive := forall x y, R x y -> R x =1 R y.
Definition right_transitive := forall x y, R x y -> R^~ x =1 R^~ y.
End RelationProperties.
Lemma rev_trans : forall T (R : rel T),
transitive R -> transitive (fun x y => R y x).
Proof. eby red; intros; eapply H. Qed.
Notation Local "{ 'all1' P }" := (forall x, P x : Prop) (at level 0).
Notation Local "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0).
Notation Local "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0).
Notation Local ph := (phantom _).
Section LocalProperties.
Variables T1 T2 T3 : Type.
Variables (d1 : mem_pred T1) (d2 : mem_pred T2) (d3 : mem_pred T3).
Notation Local ph := (phantom Prop).
Definition prop_for (x : T1) P (_ : ph {all1 P}) := P x.
Lemma forE : forall x P phP, @prop_for x P phP = P x.
Proof. done. Qed.
Definition prop_in1 P (_ : ph {all1 P}) :=
forall x, in_mem x d1 -> P x.
Definition prop_in11 P (_ : ph {all2 P}) :=
forall x y, in_mem x d1 -> in_mem y d2 -> P x y.
Definition prop_in2 P (_ : ph {all2 P}) :=
forall x y, in_mem x d1 -> in_mem y d1 -> P x y.
Definition prop_in111 P (_ : ph {all3 P}) :=
forall x y z, in_mem x d1 -> in_mem y d2 -> in_mem z d3 -> P x y z.
Definition prop_in12 P (_ : ph {all3 P}) :=
forall x y z, in_mem x d1 -> in_mem y d2 -> in_mem z d2 -> P x y z.
Definition prop_in21 P (_ : ph {all3 P}) :=
forall x y z, in_mem x d1 -> in_mem y d1 -> in_mem z d2 -> P x y z.
Definition prop_in3 P (_ : ph {all3 P}) :=
forall x y z, in_mem x d1 -> in_mem y d1 -> in_mem z d1 -> P x y z.
Variable f : T1 -> T2.
Definition prop_on1 Pf P (_ : phantom T3 (Pf f)) (_ : ph {all1 P}) :=
forall x, in_mem (f x) d2 -> P x.
Definition prop_on2 Pf P (_ : phantom T3 (Pf f)) (_ : ph {all2 P}) :=
forall x y, in_mem (f x) d2 -> in_mem (f y) d2 -> P x y.
End LocalProperties.
Implicit Arguments prop_in1 [T1 P].
Implicit Arguments prop_in11 [T1 T2 P].
Implicit Arguments prop_in2 [T1 P].
Implicit Arguments prop_in111 [T1 T2 T3 P].
Implicit Arguments prop_in12 [T1 T2 P].
Implicit Arguments prop_in21 [T1 T2 P].
Implicit Arguments prop_in3 [T1 P].
Implicit Arguments prop_on1 [T1 T2 T3 f Pf P].
Implicit Arguments prop_on2 [T1 T2 T3 f Pf P].
Definition inPhantom := Phantom Prop.
Definition onPhantom T P (x : T) := Phantom Prop (P x).
Definition bijective_in aT rT (d : mem_pred aT) (f : aT -> rT) :=
exists2 g, prop_in1 d (inPhantom (cancel f g))
& prop_on1 d (Phantom _ (cancel g)) (onPhantom (cancel g) f).
Definition bijective_on aT rT (cd : mem_pred rT) (f : aT -> rT) :=
exists2 g, prop_on1 cd (Phantom _ (cancel f)) (onPhantom (cancel f) g)
& prop_in1 cd (inPhantom (cancel g f)).
Notation "{ 'for' x , P }" :=
(prop_for x (inPhantom P))
(at level 0, format "{ 'for' x , P }") : type_scope.
Notation "{ 'in' d , P }" :=
(prop_in1 (mem d) (inPhantom P))
(at level 0, format "{ 'in' d , P }") : type_scope.
Notation "{ 'in' d1 & d2 , P }" :=
(prop_in11 (mem d1) (mem d2) (inPhantom P))
(at level 0, format "{ 'in' d1 & d2 , P }") : type_scope.
Notation "{ 'in' d & , P }" :=
(prop_in2 (mem d) (inPhantom P))
(at level 0, format "{ 'in' d & , P }") : type_scope.
Notation "{ 'in' d1 & d2 & d3 , P }" :=
(prop_in111 (mem d1) (mem d2) (mem d3) (inPhantom P))
(at level 0, format "{ 'in' d1 & d2 & d3 , P }") : type_scope.
Notation "{ 'in' d1 & & d3 , P }" :=
(prop_in21 (mem d1) (mem d3) (inPhantom P))
(at level 0, format "{ 'in' d1 & & d3 , P }") : type_scope.
Notation "{ 'in' d1 & d2 & , P }" :=
(prop_in12 (mem d1) (mem d2) (inPhantom P))
(at level 0, format "{ 'in' d1 & d2 & , P }") : type_scope.
Notation "{ 'in' d & & , P }" :=
(prop_in3 (mem d) (inPhantom P))
(at level 0, format "{ 'in' d & & , P }") : type_scope.
Notation "{ 'on' cd , P }" :=
(prop_on1 (mem cd) (inPhantom P) (inPhantom P))
(at level 0, format "{ 'on' cd , P }") : type_scope.
Notation "{ 'on' cd & , P }" :=
(prop_on2 (mem cd) (inPhantom P) (inPhantom P))
(at level 0, format "{ 'on' cd & , P }") : type_scope.
Notation "{ 'on' cd , P & g }" :=
(prop_on1 (mem cd) (Phantom (_ -> Prop) P) (onPhantom P g))
(at level 0, format "{ 'on' cd , P & g }") : type_scope.
Notation "{ 'in' d , 'bijective' f }" := (bijective_in (mem d) f)
(at level 0, f at level 8,
format "{ 'in' d , 'bijective' f }") : type_scope.
Notation "{ 'on' cd , 'bijective' f }" := (bijective_on (mem cd) f)
(at level 0, f at level 8,
format "{ 'on' cd , 'bijective' f }") : type_scope.
Section LocalGlobal.
Variables T1 T2 T3 : predArgType.
Variables (D1 : pred T1) (D2 : pred T2) (D3 : pred T3).
Variables (d1 d1' : mem_pred T1) (d2 d2' : mem_pred T2) (d3 d3' : mem_pred T3).
Variables (f f' : T1 -> T2) (g : T2 -> T1) (h : T3).
Variables (P1 : T1 -> Prop) (P2 : T1 -> T2 -> Prop).
Variable P3 : T1 -> T2 -> T3 -> Prop.
Variable Q1 : (T1 -> T2) -> T1 -> Prop.
Variable Q1l : (T1 -> T2) -> T3 -> T1 -> Prop.
Variable Q2 : (T1 -> T2) -> T1 -> T1 -> Prop.
Hypothesis sub1 : sub_mem d1 d1'.
Hypothesis sub2 : sub_mem d2 d2'.
Hypothesis sub3 : sub_mem d3 d3'.
Lemma in1W : {all1 P1} -> {in D1, {all1 P1}}.
Proof. by red. Qed.
Lemma in2W : {all2 P2} -> {in D1 & D2, {all2 P2}}.
Proof. by red. Qed.
Lemma in3W : {all3 P3} -> {in D1 & D2 & D3, {all3 P3}}.
Proof. by red. Qed.
Lemma in1T : {in T1, {all1 P1}} -> {all1 P1}.
Proof. auto. Qed.
Lemma in2T : {in T1 & T2, {all2 P2}} -> {all2 P2}.
Proof. auto. Qed.
Lemma in3T : {in T1 & T2 & T3, {all3 P3}} -> {all3 P3}.
Proof. auto. Qed.
Lemma sub_in1 : forall Ph : ph {all1 P1},
prop_in1 d1' Ph -> prop_in1 d1 Ph.
Proof. by intros ? allP x; move/sub1; apply allP. Qed.
Lemma sub_in11 : forall Ph : ph {all2 P2},
prop_in11 d1' d2' Ph -> prop_in11 d1 d2 Ph.
Proof. by intros ? allP x1 x2; move/sub1; intro d1x1; move/sub2; apply allP. Qed.
Lemma sub_in111 : forall Ph : ph {all3 P3},
prop_in111 d1' d2' d3' Ph -> prop_in111 d1 d2 d3 Ph.
Proof.
intros ? allP x1 x2 x3.
by move/sub1; intro; move/sub2; intro; move/sub3; apply allP.
Qed.
Let allQ1 f'' := {all1 Q1 f''}.
Let allQ1l f'' h' := {all1 Q1l f'' h'}.
Let allQ2 f'' := {all2 Q2 f''}.
Lemma on1W : allQ1 f -> {on D2, allQ1 f}.
Proof. by red. Qed.
Lemma on1lW : allQ1l f h -> {on D2, allQ1l f & h}.
Proof. by red. Qed.
Lemma on2W : allQ2 f -> {on D2 &, allQ2 f}.
Proof. by red. Qed.
Lemma on1T : {on T2, allQ1 f} -> allQ1 f.
Proof. red; auto. Qed.
Lemma on1lT : {on T2, allQ1l f & h} -> allQ1l f h.
Proof. red; auto. Qed.
Lemma on2T : {on T2 &, allQ2 f} -> allQ2 f.
Proof. red; auto. Qed.
Lemma subon1 : forall (Phf : ph (allQ1 f)) (Ph : ph (allQ1 f)),
prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph.
Proof. by intros ? ? allQ x; move/sub2; apply allQ. Qed.
Lemma subon1l : forall (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)),
prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph.
Proof. by intros ? ? allQ x; move/sub2; apply allQ. Qed.
Lemma subon2 : forall (Phf : ph (allQ2 f)) (Ph : ph (allQ2 f)),
prop_on2 d2' Phf Ph -> prop_on2 d2 Phf Ph.
Proof. by intros ? ? allQ x y; move/sub2; intro; move/sub2; apply allQ. Qed.
Lemma can_in_inj : {in D1, cancel f g} -> {in D1 &, injective f}.
Proof. intros fK x y; do 2 (move/fK; intro); congruence. Qed.
Lemma canLR_in : forall x y,
{in D1, cancel f g} -> y \in D1 -> x = f y -> g x = y.
Proof. by intros x y fK D1y ->; rewrite fK. Qed.
Lemma canRL_in : forall x y,
{in D1, cancel f g} -> x \in D1 -> f x = y -> x = g y.
Proof. by intros x y fK D1x <-; rewrite fK. Qed.
Lemma on_can_inj : {on D2, cancel f & g} -> {on D2 &, injective f}.
Proof. intros fK x y; do 2 (move/fK; intro); congruence. Qed.
Lemma canLR_on : forall x y,
{on D2, cancel f & g} -> f y \in D2 -> x = f y -> g x = y.
Proof. by intros x y fK D2fy ->; rewrite fK. Qed.
Lemma canRL_on : forall x y,
{on D2, cancel f & g} -> f x \in D2 -> f x = y -> x = g y.
Proof. by intros x y fK D2fx <-; rewrite fK. Qed.
Lemma inW_bij : bijective f -> {in D1, bijective f}.
Proof. by destruct 1 as [g']; exists g'; red; auto. Qed.
Lemma onW_bij : bijective f -> {on D2, bijective f}.
Proof. by destruct 1 as [g']; exists g'; red; auto. Qed.
Lemma inT_bij : {in T1, bijective f} -> bijective f.
Proof. destruct 1 as [g']; exists g'; red; auto. Qed.
Lemma onT_bij : {on T2, bijective f} -> bijective f.
Proof. destruct 1 as [g']; exists g'; red; auto. Qed.
Lemma sub_in_bij : forall D1' : pred T1,
{subset D1 <= D1'} -> {in D1', bijective f} -> {in D1, bijective f}.
Proof. destruct 2 as [g']; eexists g'; red; auto. Qed.
Lemma subon_bij : forall D2' : pred T2,
{subset D2 <= D2'} -> {on D2', bijective f} -> {on D2, bijective f}.
Proof. destruct 2 as [g']; eexists g'; red; auto. Qed.
End LocalGlobal.
Lemma sub_in2 : forall T d d' (P : T -> T -> Prop),
sub_mem d d' -> forall Ph : ph {all2 P}, prop_in2 d' Ph -> prop_in2 d Ph.
Proof. by intros until 1; apply sub_in11. Qed.
Lemma sub_in3 : forall T d d' (P : T -> T -> T -> Prop),
sub_mem d d' -> forall Ph : ph {all3 P}, prop_in3 d' Ph -> prop_in3 d Ph.
Proof. by intros until 1; apply sub_in111. Qed.
Lemma sub_in12 : forall T1 T d1 d1' d d' (P : T1 -> T -> T -> Prop),
sub_mem d1 d1' -> sub_mem d d' ->
forall Ph : ph {all3 P}, prop_in12 d1' d' Ph -> prop_in12 d1 d Ph.
Proof. by intros until 2; apply sub_in111. Qed.
Lemma sub_in21 : forall T T3 d d' d3 d3' (P : T -> T -> T3 -> Prop),
sub_mem d d' -> sub_mem d3 d3' ->
forall Ph : ph {all3 P}, prop_in21 d' d3' Ph -> prop_in21 d d3 Ph.
Proof. by intros until 2; apply sub_in111. Qed.
Comparison for nat
Fixpoint eqn_rec (x y: nat) {struct x} :=
match x, y with
| O, O => true
| S x, S y => eqn_rec x y
| _, _ => false
end.
Definition eqn := match tt with tt => eqn_rec end.
Lemma eqnP: forall x y, reflect (x = y) (eqn x y).
Proof.
induction[] x [y]; vauto.
change (eqn (S x) (S y)) with (eqn x y).
case IHx; constructor; congruence.
Qed.
Canonical Structure nat_eqMixin := EqMixin eqnP.
Canonical Structure nat_eqType := Eval hnf in EqType nat nat_eqMixin.
Lemma eqnE : eqn = (@eq_op _).
Proof. done. Qed.
Comparison for option
Definition eq_option {A: eqType} (x y: option A) :=
match x, y with None, None => true
| Some x, Some y => x == y
| _ , _ => false
end.
Lemma eq_optionP: forall (A: eqType) (x y: option A), reflect (x = y) (eq_option x y).
Proof.
induction[] x [y]; ins; vauto.
case eqP; ins; vauto.
constructor; congruence.
Qed.
Canonical Structure option_eqMixin A := EqMixin (@eq_optionP A).
Canonical Structure option_eqType (A: eqType) := Eval hnf in EqType (option A) (@option_eqMixin A).
This page has been generated by coqdoc