Library Ssreflect.ssreflect

Declare ML Module "ssreflect".
Require Import Bool.

Set Implicit Arguments.
Unset Strict Implicit.

Module SsrSyntax.


Reserved Notation "(* x 'is' y 'by' z 'of' // /= //= *)" (at level 8).
Reserved Notation "(* 69 *)" (at level 69).

End SsrSyntax.

Export SsrSyntax.


Delimit Scope general_if_scope with GEN_IF.

Notation "'if' c 'then' v1 'else' v2" :=
  (if c then v1 else v2)
  (at level 200, c, v1, v2 at level 200, only parsing) : general_if_scope.

Notation "'if' c 'return' t 'then' v1 'else' v2" :=
  (if c return t then v1 else v2)
  (at level 200, c, t, v1, v2 at level 200, only parsing) : general_if_scope.

Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" :=
  (if c as x return t then v1 else v2)
  (at level 200, c, t, v1, v2 at level 200, x ident, only parsing)
     : general_if_scope.


Delimit Scope boolean_if_scope with BOOL_IF.

Notation "'if' c 'return' t 'then' v1 'else' v2" :=
  (if c%bool is true in bool return t then v1 else v2) : boolean_if_scope.

Notation "'if' c 'then' v1 'else' v2" :=
  (if c%bool is true in bool return _ then v1 else v2) : boolean_if_scope.

Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" :=
  (if c%bool is true as x in bool return t then v1 else v2) : boolean_if_scope.

Open Scope boolean_if_scope.

Delimit Scope form_scope with FORM.
Open Scope form_scope.

Notation "T : 'Type'" := (T%type : Type) (at level 100, only parsing).


Module TheCanonical.

CoInductive put vT sT (v1 v2 : vT) (s : sT) : Type := Put.

Definition get vT sT v s (p : @put vT sT v v s) := let: Put := p in s.

Definition get_by vT sT of sT -> vT := @get vT sT.

End TheCanonical.

Import TheCanonical.
Notation "[ 'the' sT 'of' v 'by' f ]" :=
  (@get_by _ sT f _ _ ((fun v' (s : sT) => Put v' (f s) s) v _))
  (at level 0, only parsing) : form_scope.

Notation "[ 'the' sT 'of' v ]" := (get ((fun s : sT => Put v s s) _))
  (at level 0, only parsing) : form_scope.


Notation "[ 'th' 'e' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _)
  (at level 0, format "[ 'th' 'e' sT 'of' v 'by' f ]") : form_scope.

Notation "[ 'th' 'e' sT 'of' v ]" := (@get _ sT v _ _)
  (at level 0, format "[ 'th' 'e' sT 'of' v ]") : form_scope.



Definition argumentType T P & forall x : T, P x := T.
Definition dependentReturnType T P & forall x : T, P x := P.
Definition returnType aT rT & aT -> rT := rT.

Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s)
  (at level 0, format "{ 'type' 'of' c 'for' s }") : type_scope.


CoInductive phantom (T : Type) (p : T) : Type := Phantom.
Implicit Arguments phantom [].
CoInductive phant (p : Type) : Type := Phant.


Definition protect_term (A : Type) (x : A) : A := x.

Term tagging (user-level).

Notation "'nosimpl' t" := (let: tt := tt in t) (at level 10, t at level 8).

Structure unlockable (T : Type) (v : T) : Type :=
  Unlockable {unlocked : T; _ : unlocked = v}.

Lemma unlock : forall aT rT (f : forall x : aT, rT x) (u : unlockable f) x,
  unlocked u x = f x.
Proof. move=> aT rT f [u /= ->]; split. Qed.


Lemma master_key : unit. Proof. exact tt. Qed.

Definition locked A := let: tt := master_key in fun x : A => x.

Lemma lock : forall A x, x = locked x :> A.
Proof. rewrite /locked; case master_key; split. Qed.

Lemma not_locked_false_eq_true : locked false <> true.
Proof. rewrite -lock; discriminate. Qed.

Ltac done :=
  trivial; hnf; intros; solve
   [ do ![solve [trivial | apply: sym_equal; trivial]
         | discriminate | contradiction | split]
   | case not_locked_false_eq_true; assumption
   | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].


Definition ssr_have Plemma Pgoal (step : Plemma) rest : Pgoal := rest step.
Implicit Arguments ssr_have [Pgoal].

Definition ssr_suff Plemma Pgoal step (rest : Plemma) : Pgoal := step rest.
Implicit Arguments ssr_suff [Pgoal].

Definition ssr_wlog := ssr_suff.
Implicit Arguments ssr_wlog [Pgoal].


Fixpoint nary_congruence_statement (n : nat)
         : (forall B, (B -> B -> Prop) -> Prop) -> Prop :=
  match n with
  | O => fun k => forall B, k B (fun x1 x2 : B => x1 = x2)
  | S n' =>
    let k' A B e (f1 f2 : A -> B) :=
      forall x1 x2, x1 = x2 -> (e (f1 x1) (f2 x2) : Prop) in
    fun k => forall A, nary_congruence_statement n' (fun B e => k _ (k' A B e))
  end.

Lemma nary_congruence : forall n : nat,
 let k B e := forall y : B, (e y y : Prop) in nary_congruence_statement n k.
Proof.
move=> n k; have: k _ _ := _; rewrite {1}/k.
elim: n k => [|n IHn] k Hk /= A; auto.
by apply: IHn => B e He; apply: Hk => f x1 x2 <-.
Qed.


Section ApplyIff.

Variables P Q : Prop.
Hypothesis eqPQ : P <-> Q.

Lemma iffLR : P -> Q. Proof. by case eqPQ. Qed.
Lemma iffRL : Q -> P. Proof. by case eqPQ. Qed.

Lemma iffLRn : ~P -> ~Q. Proof. by move=> nP tQ; case: nP; case: eqPQ tQ. Qed.
Lemma iffRLn : ~Q -> ~P. Proof. by move=> nQ tP; case: nQ; case: eqPQ tP. Qed.

End ApplyIff.

Hint View for move/ iffLRn|2 iffRLn|2 iffLR|2 iffRL|2.
Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2.

Unset Implicit Arguments.