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.

Set Implicit Arguments.

Axioms


Require ClassicalFacts.
Require Export FunctionalExtensionality.
Require Export ProofIrrelevance.

Ltac exten := apply functional_extensionality.

Coersion of bool into Prop


Coersion of bools into Prop
Coercion is_true (b : bool) : Prop := b = true.

Hints for auto
Lemma vlib__true_is_true : true.

Lemma vlib__not_false_is_true : ¬ false.

Hint Resolve vlib__true_is_true vlib__not_false_is_true.

Very basic automation


Set up for basic simplification


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).

Boolean reflection


These definitions are ported from ssr-bool.
Negation lemmas
Section NegationLemmas.

  Variables (b c : bool).

  Lemma negbT : b = false negb b.
  Lemma negbTE: negb b b = false.
  Lemma negbF : b negb b = false.
  Lemma negbFE: negb b = false b.
  Lemma negbNE: negb (negb b) b.

  Lemma negbLR : b = negb c negb b = c.

  Lemma negbRL : negb b = c b = negb c.

  Lemma contra : (c b) negb b negb c.

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.

Lemma if_same : (if b then vT else vT) = vT.

Lemma if_neg : (if negb b then vT else vF) = if b then vF else vT.

Lemma fun_if : f (if b then vT else vF) = if b then f vT else f vF.

Lemma if_arg : fT fF : A B,
  (if b then fT else fF) x = if b then fT x else fF x.

End BoolIf.

The reflection predicate
Inductive reflect (P : Prop) : bool Set :=
  | 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.

Lemma introTF : (if c then P else ¬ P) b = c.

Lemma elimNTF : negb b = c if c then ¬ P else P.

Lemma elimTF : b = c if c then P else ¬ P.

Lemma equivPif : (Q P) (P Q) if b then Q else ¬ Q.

Lemma xorPif : Q P ¬ (Q P) if b then ¬ Q else Q.

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.

Lemma elimTFn : b = c if c then ¬ P else P.

Lemma equivPifn : (Q P) (P Q) if b then ¬ Q else Q.

Lemma xorPifn : Q P ¬ (Q P) if b then Q else ¬ Q.

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.
Lemma introF : ¬ P b = false.
Lemma introN : ¬ P negb b.
Lemma introNf : P negb b = false.
Lemma introTn : ¬ P b'.
Lemma introFn : P b' = false.

Lemma elimT : b P.
Lemma elimF : b = false ¬ P.
Lemma elimN : negb b ¬P.
Lemma elimNf : negb b = false P.
Lemma elimTn : b' ¬ P.
Lemma elimFn : b' = false P.

Lemma introP : (b Q) (negb b ¬ Q) reflect Q b.

Lemma iffP : (P Q) (Q P) reflect Q b.

Lemma appP : reflect Q b P Q.

Lemma sameP : reflect P c b = c.

Lemma decPcases : if b then P else ¬ P.

Definition decP : {P} + {¬ P}.

End Reflect.

Coercion elimT : reflect >-> Funclass.

Section ReflectConnectives.

Variable b1 b2 b3 b4 b5 : bool.

Lemma idP : reflect b1 b1.

Lemma idPn : reflect (negb b1) (negb b1).

Lemma negP : reflect (¬ b1) (negb b1).

Lemma negPn : reflect b1 (negb (negb b1)).

Lemma negPf : reflect (b1 = false) (negb b1).

Lemma andP : reflect (b1 b2) (b1 && b2).

Lemma orP : reflect (b1 b2) (b1 || b2).

Lemma nandP : reflect (negb b1 negb b2) (negb (b1 && b2)).

Lemma norP : reflect (negb b1 negb b2) (negb (b1 || b2)).

End ReflectConnectives.

Equality types


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 : Tx).

Module Equality.

Definition axiom T (e : T T bool) := 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}.
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 : T x, eq_op x = Equality.op (Equality.class T) x.

Lemma eqP : T, Equality.axiom (@eq_op T).
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 :
   (T: eqType) (x y : T), reflect (x = y) (x == y).

Lemma neqP : (T: eqType) (x y: T), reflect (x y) (x != y).

Lemma beq_refl : (T : eqType) (x : T), x == x.

Lemma beq_sym : (T : eqType) (x y : T), (x == y) = (y == x).

Hint Resolve beq_refl : vlib.
Hint Rewrite beq_refl : vlib_trivial.

Notation eqxx := beq_refl.


Basic simplification tactics


Lemma vlib__negb_rewrite : b, negb b b = false.

Lemma vlib__andb_split : b1 b2, b1 && b2 b1 b2.

Lemma vlib__nandb_split : b1 b2, b1 && b2 = false b1 = false b2 = false.

Lemma vlib__orb_split : b1 b2, b1 || b2 b1 b2.

Lemma vlib__norb_split : b1 b2, b1 || b2 = false b1 = false b2 = false.

Lemma vlib__eqb_split : b1 b2 : bool, (b1 b2) (b2 b1) b1 = b2.

Lemma vlib__beq_rewrite : (T : eqType) (x1 x2 : T), x1 == x2 x1 = x2.

Set up for basic simplification: database of reflection lemmas


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 A (P: unit A) : A := P tt.

Notation "<< x : t >>" := (NW (fun xt)) (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 : x, NW (fun y_) |- _
      let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
    | H : 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 : x, NW (fun y_) |- _
      let x' := fresh x in let y' := fresh y in destruct H as [x' y']; red in y'
    | H : 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 in (_ = 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 in (_ = 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.

Delineating cases in proofs


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.

Exploiting a hypothesis


Exploit an assumption (adapted from CompCert).

Ltac exploit x :=
    refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _ _) _)
 || refine ((fun x yy x) (x _ _ _) _)
 || refine ((fun x yy x) (x _ _) _)
 || refine ((fun x yy x) (x _) _).

Induction


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 ].

Views


Ltac vlib__apply_refl :=
  intros;
    match goal with
      | |- is_true ?peapply introT; [solve [trivial with vlib_refl]|]
      | |- ?p = trueeapply introT; [solve [trivial with vlib_refl]|]
      | |- ?p = falseeapply introFn; [solve [trivial with vlib_refl]|]
      | |- ?p = falseeapply 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/" := vlib__move_refl.

Tactic Notation "move/" constr(X) ident_list(Y) := revert Y; vlib__move_with X.

case

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/" := vlib__case_refl.

Tactic Notation "case/" constr(X) ident_list(Y) := revert Y; vlib__case_with X.

double apply

Tactic Notation "apply/" constr(X1) "/" constr(X2) :=
  eapply sameP; [apply X1; edone|eapply iffP; [apply X2; edone|instantiate|instantiate]].

Function notation ported from ssrfun.v


Delimit Scope fun_scope with FUN.
Open Scope fun_scope.

Notation "f ^~ y" := (fun xf 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 yf y
    | Nonex
  end.

Definition default T := apply (fun x : Tx).

Definition bind aT rT (f : aT option rT) := apply f None.

Definition map aT rT (f : aT rT) := bind (fun xSome (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 xmatch f with SimplFun lamlam x end.

Coercion fun_of_simpl : simpl_fun >-> Funclass.

End SimplFun.

Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : TE))
  (at level 0,
   format "'[hv' [ 'fun' : T => '/ ' E ] ']'") : fun_scope.

Notation "[ 'fun' x => E ]" := (SimplFun (fun xE))
  (at level 0, x ident,
   format "'[hv' [ 'fun' x => '/ ' E ] ']'") : fun_scope.

Notation "[ 'fun' x : T => E ]" := (SimplFun (fun x : TE))
  (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) := x, x = x0.

Lemma unitE : all_equal_to tt.

A generic wrapper type

Structure wrapped T := Wrap {unwrap : T}.
Canonical Structure wrap T x := @Wrap T x.


Extensional equality for unary and binary functions + syntactic sugar.

Section ExtensionalEquality.

Variables A B C : Type.

Definition eqfun (f g : B A) : Prop := x, f x = g x.

Definition eqrel (r s : C B A) : Prop := x y, r x y = s x y.

Lemma frefl : f, eqfun f f.

Lemma fsym : f g, eqfun f g eqfun g f.

Lemma ftrans : f g h (EQ1: eqfun f g) (EQ2: eqfun g h), eqfun f h.

Lemma rrefl : r, eqrel r r.

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 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 ttf (g x) end.

Definition pcomp (f : B option A) (g : C option B) x := obind f (g x).

Lemma eq_comp : f f' g g', f =1 f' g =1 g' comp f g =1 comp f' g'.

End Composition.

Notation "[ 'eta' f ]" := (fun xf x)
  (at level 0, format "[ 'eta' f ]") : fun_scope.

Notation id := (fun xx).
Notation "@ 'id' T " := (fun x : Tx)
  (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 := x, f (aF x) = rF (f x).
Definition morphism_2 aOp rOp := x y, f (aOp x y) = rOp (f x) (f y).

End Morphism.

Notation "{ 'morph' f : x / a >-> r }" :=
  (morphism_1 f (fun xa) (fun xr))
  (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 xa) (fun xa))
  (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 ya) (fun x yr))
  (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 ya) (fun x ya))
  (at level 0, f at level 99, x ident, y ident,
   format "{ 'morph' f : x y / a }") : type_scope.

Properties of relations (ported from ssrfun.v)


Section Injections.

Variables (rT aT : Type) (f : aT rT).

Definition injective := x1 x2, f x1 = f x2 x1 = x2.

Definition cancel g := x, g (f x) = x.

Definition pcancel g := x, g (f x) = Some x.

Definition ocancel (g : aT option rT) h := x, oapp h x (g x) = x.

Lemma can_pcan : g, cancel g pcancel (fun ySome (g y)).

Lemma pcan_inj : g, pcancel g injective.

Lemma can_inj : g, cancel g injective.

Lemma canLR : g x y, cancel g x = f y g x = y.

Lemma canRL : g x y, cancel g f x = y x = g y.

End Injections.

Lemma esymK : T x y, cancel (@eq_sym T x y) (@eq_sym T y x).

Lemma etrans_id : T x y (eqxy : x = y :> T),
  eq_trans (eq_refl x) eqxy = eqxy.

Section InjectionsTheory.

Variables (A B C : Type) (f g : B A) (h : C B).

Lemma inj_id : injective (@id A).

Lemma inj_can_sym : f', cancel f f' injective f' cancel f' f.

Lemma inj_comp : injective f injective h injective (f \o h).

Lemma can_comp : f' h',
  cancel f f' cancel h h' cancel (f \o h) (h' \o f').

Lemma pcan_pcomp : f' h',
  pcancel f f' pcancel h h' pcancel (f \o h) (pcomp h' f').

Lemma eq_inj : injective f f =1 g injective g.

Lemma eq_can : f' g', cancel f f' f =1 g f' =1 g' cancel g g'.

Lemma inj_can_eq : f',
  cancel f f' injective f' cancel g f' f =1 g.

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.

Lemma bij_can_sym : f', cancel f' f cancel f f'.

Lemma bij_can_eq : f' f'', cancel f f' cancel f f'' f' =1 f''.

End Bijections.

Section BijectionsTheory.

Variables (A B C : Type) (f : B A) (h : C B).

Lemma eq_bij : bijective f g, f =1 g bijective g.

Lemma bij_comp : bijective f bijective h bijective (f \o h).

Lemma bij_can_bij : bijective f f', cancel f f' bijective f'.

End BijectionsTheory.

Section Involutions.

Variables (A : Type) (f : A A).

Definition involutive := cancel f f.

Hypothesis Hf : involutive.

Lemma inv_inj : injective f.

Lemma inv_bij : bijective f.

End Involutions.

Section OperationProperties.

Variables S T R : Type.

Section SopTisR.
Implicit Type op : S T R.
Definition left_inverse e inv op := x, op (inv x) x = e.
Definition right_inverse e inv op := x, op x (inv x) = e.
End SopTisR.

Section SopTisS.
Implicit Type op : S T S.
Definition right_id e op := x, op x e = x.
Definition left_zero z op := x, op z x = z.
Definition right_commutative op := x y z, op (op x y) z = op (op x z) y.
Definition left_distributive op add :=
   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 := x, op e x = x.
Definition right_zero z op := x, op x z = z.
Definition left_commutative op := x y z, op x (op y z) = op y (op x z).
Definition right_distributive op add :=
   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 := x, op x x = e.
Definition commutative op := x y, op x y = op y x.
End SopSisT.

Section SopSisS.
Implicit Type op : S S S.
Definition idempotent op := x, op x x = x.
Definition associative op := x y z, op x (op y z) = op (op x y) z.
End SopSisS.

End OperationProperties.

Boolean laws

Shorter, more systematic names for the boolean connectives laws.

Lemma andTb : x, true && x = x.
Lemma andFb : x, false && x = false.
Lemma andbT : x, x && true = x.
Lemma andbF : x, x && false = false.
Lemma andbb : x, x && x = x.

Lemma andbC : x y, x && y = y && x.
Lemma andbA : x y z, x && (y && z) = x && y && z.
Lemma andbCA : x y z, x && (y && z) = y && (x && z).
Lemma andbAC : x y z, x && y && z = x && z && y.

Lemma andbN : b, b && negb b = false.
Lemma andNb : b, negb b && b = false.

Lemma orTb : x, true || x = true.
Lemma orFb : x, false || x = x.
Lemma orbT : x, x || true = true.
Lemma orbF : x, x || false = x.
Lemma orbb : x, x || x = x.

Lemma orbC : x y, x || y = y || x.
Lemma orbA : x y z, x || (y || z) = x || y || z.
Lemma orbCA : x y z, x || (y || z) = y || (x || z).
Lemma orbAC : x y z, x || y || z = x || z || y.

Lemma orbN : b, b || negb b = true.
Lemma orNb : b, negb b || b = true.

Lemma andb_orl : x y z, (x || y) && z = x && z || y && z.
Lemma andb_orr : x y z, x && (y || z) = x && y || x && z.
Lemma orb_andl : x y z, (x && y) || z = (x || z) && (y || z).
Lemma orb_andr : x y z, x || (y && z) = (x || y) && (x || z).

Pseudo-cancellation -- i.e, absorbtion

Lemma andbK : b1 b2, b1 && b2 || b1 = b1.
Lemma andKb : b1 b2, b1 || b2 && b1 = b1.
Lemma orbK : b1 b2, (b1 || b2) && b1 = b1.
Lemma orKb : b1 b2, b1 && (b2 || b1) = b1.

Exclusive or -- xorb

Lemma xorFb : x, xorb false x = x.
Lemma xorbF : x, xorb x false = x.
Lemma xorTb : x, xorb true x = negb x.
Lemma xorbT : x, xorb x true = negb x.
Lemma xorbb : x, xorb x x = false.

Lemma xorbC : x y, xorb x y = xorb y x.
Lemma xorbA : x y z, xorb x (xorb y z) = xorb (xorb x y) z.
Lemma xorbCA : x y z, xorb x (xorb y z) = xorb y (xorb x z).
Lemma xorbAC : x y z, xorb (xorb x y) z = xorb (xorb x z) y.

Lemma xorbN : x y, xorb x (negb y) = negb (xorb x y).
Lemma xorNb : x y, xorb x (negb y) = negb (xorb x y).

Lemma andb_xorl : x y z, (xorb x y) && z = xorb (x && z) (y && z).
Lemma andb_xorr : x y z, x && (xorb y z) = xorb (x && y) (x && z).

Negation

Lemma negb_neg : x, negb (negb x) = x.
Lemma negb_and : x y, negb (x && y) = negb x || negb y.
Lemma negb_or : x y, negb (x || y) = negb x && negb y.
Lemma negb_xor : x y, negb (xorb x y) = xorb (negb x) y.

Automation support


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.

Other potentially useful rewrites: negb_and negb_or negb_xor.

Views


An attempt to replicate functionality from ss-reflect.

Section ApplyIff.

Variables P Q : Prop.
Hypothesis eqPQ : P Q.

Lemma iffLR : P Q.

Lemma iffRL : Q P.

Lemma iffLRn : ¬P ¬Q.

Lemma iffRLn : ¬Q ¬P.

End ApplyIff.

Predicates, i.e. functions to bool (ported from ssrbool.v)



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 _) xp1 x && p2 x).
Notation xpredU := (fun (p1 p2 : pred _) xp1 x || p2 x).
Notation xpredC := (fun (p : pred _) xnegb (p x)).
Notation xpredD := (fun (p1 p2 : pred _) xnegb (p2 x) && p1 x).
Notation xpreim := (fun f (p : pred _) xp (f x)).
Notation xrelU := (fun (r1 r2 : rel _) x yr1 x y || r2 x y).

Section Predicates.

Variables T : Type.

Definition subpred (p1 p2 : pred T) := x, p1 x p2 x.

Definition subrel (r1 r2 : rel T) := 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 yr x y.

Definition relU r1 r2 := SimplRel (xrelU r1 r2).

Lemma subrelUl : r1 r2, subrel r1 (relU r1 r2).

Lemma subrelUr : r1 r2, subrel r2 (relU r1 r2).

Inductive mem_pred : Type := Mem (_ : pred T).

Definition isMem pT topred mem :=
  mem = (fun p : pTMem (fun xtopred 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 pfun xp 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 _ : TE))
  (at level 0, format "[ 'pred' : T | E ]") : fun_scope.
Notation "[ 'pred' x | E ]" := (SimplPred (fun xE))
  (at level 0, x ident, format "[ 'pred' x | E ]") : fun_scope.
Notation "[ 'pred' x : T | E ]" := (SimplPred (fun x : TE))
  (at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'rel' x y | E ]" := (SimplRel (fun x yE))
  (at level 0, x ident, y ident, format "[ 'rel' x y | E ]") : fun_scope.
Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : TE))
  (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 := x : T, in_mem x p1 = in_mem x p2.
Definition sub_mem T p1 p2 := 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 : (p : pT), mem (topred p) = mem p.

Lemma topredE : x (p : pT), topred p x = (x \in p).

Lemma in_simpl : x (p : simpl_pred T), (x \in p) = p x.

Lemma simpl_predE : (p : pred T), [pred x | p x] =1 p.


Lemma mem_simpl : (p : simpl_pred T), mem p = p :> pred T.

Definition memE := mem_simpl.

End simpl_mem.

Section RelationProperties.


Variable T : Type.

Variable R : rel T.

Definition total := x y, R x y || R y x.
Definition transitive := x y z, R x y R y z R x z.

Definition symmetric := x y, R x y = R y x.
Definition antisymmetric := x y, R x y R y x x = y.
Definition pre_symmetric := x y, R x y R y x.

Lemma symmetric_from_pre : pre_symmetric symmetric.

Lemma pre_from_symmetric : symmetric pre_symmetric.

Definition reflexive := x, R x x.
Definition irreflexive := x, R x x = false.

Definition left_transitive := x y, R x y R x =1 R y.
Definition right_transitive := x y, R x y R^~ x =1 R^~ y.

End RelationProperties.

Lemma rev_trans : T (R : rel T),
  transitive R transitive (fun x yR y x).


Notation Local "{ 'all1' P }" := ( x, P x : Prop) (at level 0).
Notation Local "{ 'all2' P }" := ( x y, P x y : Prop) (at level 0).
Notation Local "{ 'all3' P }" := ( 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 : x P phP, @prop_for x P phP = P x.

Definition prop_in1 P (_ : ph {all1 P}) :=
   x, in_mem x d1 P x.

Definition prop_in11 P (_ : ph {all2 P}) :=
   x y, in_mem x d1 in_mem y d2 P x y.

Definition prop_in2 P (_ : ph {all2 P}) :=
   x y, in_mem x d1 in_mem y d1 P x y.

Definition prop_in111 P (_ : ph {all3 P}) :=
   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}) :=
   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}) :=
   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}) :=
   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}) :=
   x, in_mem (f x) d2 P x.

Definition prop_on2 Pf P (_ : phantom T3 (Pf f)) (_ : ph {all2 P}) :=
   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}}.
Lemma in2W : {all2 P2} {in D1 & D2, {all2 P2}}.
Lemma in3W : {all3 P3} {in D1 & D2 & D3, {all3 P3}}.

Lemma in1T : {in T1, {all1 P1}} {all1 P1}.
Lemma in2T : {in T1 & T2, {all2 P2}} {all2 P2}.
Lemma in3T : {in T1 & T2 & T3, {all3 P3}} {all3 P3}.

Lemma sub_in1 : Ph : ph {all1 P1},
  prop_in1 d1' Ph prop_in1 d1 Ph.

Lemma sub_in11 : Ph : ph {all2 P2},
  prop_in11 d1' d2' Ph prop_in11 d1 d2 Ph.

Lemma sub_in111 : Ph : ph {all3 P3},
  prop_in111 d1' d2' d3' Ph prop_in111 d1 d2 d3 Ph.

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}.
Lemma on1lW : allQ1l f h {on D2, allQ1l f & h}.
Lemma on2W : allQ2 f {on D2 &, allQ2 f}.

Lemma on1T : {on T2, allQ1 f} allQ1 f.
Lemma on1lT : {on T2, allQ1l f & h} allQ1l f h.
Lemma on2T : {on T2 &, allQ2 f} allQ2 f.

Lemma subon1 : (Phf : ph (allQ1 f)) (Ph : ph (allQ1 f)),
  prop_on1 d2' Phf Ph prop_on1 d2 Phf Ph.

Lemma subon1l : (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)),
  prop_on1 d2' Phf Ph prop_on1 d2 Phf Ph.

Lemma subon2 : (Phf : ph (allQ2 f)) (Ph : ph (allQ2 f)),
  prop_on2 d2' Phf Ph prop_on2 d2 Phf Ph.

Lemma can_in_inj : {in D1, cancel f g} {in D1 &, injective f}.

Lemma canLR_in : x y,
  {in D1, cancel f g} y \in D1 x = f y g x = y.

Lemma canRL_in : x y,
  {in D1, cancel f g} x \in D1 f x = y x = g y.

Lemma on_can_inj : {on D2, cancel f & g} {on D2 &, injective f}.

Lemma canLR_on : x y,
  {on D2, cancel f & g} f y \in D2 x = f y g x = y.

Lemma canRL_on : x y,
  {on D2, cancel f & g} f x \in D2 f x = y x = g y.

Lemma inW_bij : bijective f {in D1, bijective f}.

Lemma onW_bij : bijective f {on D2, bijective f}.

Lemma inT_bij : {in T1, bijective f} bijective f.

Lemma onT_bij : {on T2, bijective f} bijective f.

Lemma sub_in_bij : D1' : pred T1,
  {subset D1 D1'} {in D1', bijective f} {in D1, bijective f}.

Lemma subon_bij : D2' : pred T2,
 {subset D2 D2'} {on D2', bijective f} {on D2, bijective f}.

End LocalGlobal.

Lemma sub_in2 : T d d' (P : T T Prop),
  sub_mem d d' Ph : ph {all2 P}, prop_in2 d' Ph prop_in2 d Ph.

Lemma sub_in3 : T d d' (P : T T T Prop),
  sub_mem d d' Ph : ph {all3 P}, prop_in3 d' Ph prop_in3 d Ph.

Lemma sub_in12 : T1 T d1 d1' d d' (P : T1 T T Prop),
  sub_mem d1 d1' sub_mem d d'
   Ph : ph {all3 P}, prop_in12 d1' d' Ph prop_in12 d1 d Ph.

Lemma sub_in21 : T T3 d d' d3 d3' (P : T T T3 Prop),
  sub_mem d d' sub_mem d3 d3'
   Ph : ph {all3 P}, prop_in21 d' d3' Ph prop_in21 d d3 Ph.


This page has been generated by coqdoc Imprint | Data protection