Library RelationAlgebra.common

common: basic modules, utilities, and tactics


Require Export Setoid Morphisms.
Require Import BinNums.
Set Implicit Arguments.

Bind Scope nat_scope with nat.

this lemma is useful when applied in hypotheses (apply apply in H makes it possible to specialize an hypothesis H by generating the corresponding subgoals)
Definition apply X x Y (f: X → Y) := f x.

for debugging
Ltac print_goal := match goal with |- ?x ⇒ idtac x end.

closing tactic
Ltac Now tac := tac; solve [auto].

coercion from Booleans to propositions
Coercion is_true: bool >-> Sortclass.
#[export] Hint Unfold is_true : core.

lazy Boolean connectives
Notation "a <<< b" := (if (a:bool) then (b:bool) else true) (at level 49).
Notation "a &&& b" := (if (a:bool) then (b:bool) else false) (right associativity, at level 59).
Notation "a ||| b" := (if (a:bool) then true else (b:bool)) (right associativity, at level 60).

Booleans inclusion
Definition le_bool (a b : bool) := a → b.
#[export] Hint Unfold le_bool : core.

specification in Prop of the above operations
Lemma le_bool_spec a b: is_true (a<<<b) ↔ le_bool a b.
Proof. case a; intuition. discriminate. Qed.
Lemma landb_spec a b: is_true (a&&&b) ↔ a ∧ b.
Proof. case a; intuition. discriminate. Qed.
Lemma lorb_spec a b: is_true (a|||b) ↔ a ∨ b.
Proof. case a; intuition. discriminate. Qed.
Lemma negb_spec a: is_true (negb a) ↔ a = false.
Proof. case a; intuition. Qed.

Lemma eq_bool_iff (a b: bool): (a↔b) ↔ a=b.
Proof.
  split. unfold is_true. 2: now intros <-.
  case a; case b; intuition discriminate.
Qed.

coercion from sums to Booleans
Definition bool_of_sumbool A B (c: sumbool A B): bool := if c then true else false.
Coercion bool_of_sumbool: sumbool >-> bool.

Lemma sumbool_true A (c: sumbool A (¬A)): A → c.
Proof. intro HA. case c; intro F. reflexivity. elim (F HA). Qed.

Lemma is_true_sumbool A (c: {A}+{¬A}): is_true c ↔ A.
Proof. case c; simpl; intuition; discriminate. Qed.

Lemma sumbool_iff A B: (A↔B) → {A}+{¬A} → {B}+{¬B}.
Proof. tauto. Qed.

simplifictation hints
Arguments Basics.flip {_ _ _} _ _ _/.
Arguments Basics.impl _ _ /.
Arguments Proper {_} _ _ /.
Arguments respectful {_ _} _ _ / _ _.
Arguments pointwise_relation _ {_} _ / _ _.
Arguments Transitive {_} _ /.
Arguments Symmetric {_} _ /.
Arguments Reflexive {_} _ /.
Notation flip := Basics.flip.
Notation impl := Basics.impl.
Notation pwr := (pointwise_relation _).

opaque identity, used to document impossible cases
Definition assert_false {A} (x: A): A. Proof. assumption. Qed.

2^n (defined through the double function to ease definition of finite sets as ordinals)
Fixpoint double n := match n with 0 ⇒ 0 | S n ⇒ S (S (double n)) end.
Fixpoint pow2 n := match n with 0 ⇒ 1 | S n ⇒ double (pow2 n) end.

closing tactics by reflection, without re-computing at Qed-time
Ltac close_by_reflection val := (abstract (vm_cast_no_check (eq_refl val))).

introduce non propositional variables
Ltac intro_vars :=
  match goal with
    | |- ?H → _ ⇒
      match type of H with
        | Prop ⇒ let H' := fresh in intro H'; intro_vars; revert H'
        | _ ⇒ intro; intro_vars
      end
    | |- _ ⇒ idtac
  end.

revert all propositional variables
Ltac revert_prop :=
  match goal with
    | H:?t |- _ ⇒ match type of t with Prop ⇒ revert H; revert_prop end
    | _ ⇒ idtac
  end.