Library Ssreflect.ssreflect
Require Import Bool. Require Import ssrmatching.
Set SsrAstVersion.
Global Set Asymmetric Patterns.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module SsrSyntax.
Reserved Notation "(* x 'is' y 'of' z 'isn't' // /= //= *)" (at level 8).
Reserved Notation "(* 69 *)" (at level 69).
Reserved Notation "(* Use to test if 'SsrSyntax_is_Imported' *)" (at level 8).
Reserved Notation "<hidden n >" (at level 200).
Reserved Notation "T (* n *)" (at level 200, format "T (* n *)").
End SsrSyntax.
Export SsrMatchingSyntax.
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 "x : T" := (x : T)
(at level 100, right associativity,
format "'[hv' x '/ ' : T ']'") : core_scope.
Notation "T : 'Type'" := (T%type : Type)
(at level 100, only parsing) : core_scope.
Notation "P : 'Prop'" := (P%type : Prop)
(at level 100, only parsing) : core_scope.
Definition abstract_lock := unit.
Definition abstract_key := tt.
Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) :=
let: tt := lock in statement.
Notation "<hidden n >" := (abstract _ n _).
Notation "T (* n *)" := (abstract T n abstract_key).
Module TheCanonical.
CoInductive put vT sT (v1 v2 : vT) (s : sT) := 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 & ∀ x : T, P x := T.
Definition dependentReturnType T P & ∀ 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 (p : T) := Phantom.
Implicit Arguments phantom [].
Implicit Arguments Phantom [].
CoInductive phant (p : Type) := Phant.
Definition protect_term (A : Type) (x : A) : A := x.
Notation unkeyed x := (let flex := x in flex).
Definition ssr_converse R (r : R) := (Logic.I, r).
Notation "=^~ r" := (ssr_converse r) (at level 100) : form_scope.
Notation nosimpl t := (let: tt := tt in t).
Lemma master_key : unit. Proof. exact tt. Qed.
Definition locked A := let: tt := master_key in fun x : A ⇒ x.
Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed.
Lemma not_locked_false_eq_true : locked false ≠ true.
Proof. unlock; 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 ].
Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}.
Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed.
Notation "[ 'unlockable' 'of' C ]" := (@Unlockable _ _ C (unlock _))
(at level 0, format "[ 'unlockable' 'of' C ]") : form_scope.
Notation "[ 'unlockable' 'fun' C ]" := (@Unlockable _ (fun _ ⇒ _) C (unlock _))
(at level 0, format "[ 'unlockable' 'fun' C ]") : form_scope.
Definition locked_with k := let: tt := k in fun T x ⇒ x : T.
Lemma locked_withE T k x : unkeyed (locked_with k x) = x :> T.
Proof. by case: k. Qed.
Canonical locked_with_unlockable T k x :=
@Unlockable T x (locked_with k x) (locked_withE k x).
Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T.
Proof. exact: unlock. Qed.
Definition ssr_have Plemma Pgoal (step : Plemma) rest : Pgoal := rest step.
Implicit Arguments ssr_have [Pgoal].
Definition ssr_have_let Pgoal Plemma step
(rest : let x : Plemma := step in Pgoal) : Pgoal := rest.
Implicit Arguments ssr_have_let [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)
: (∀ B, (B → B → Prop) → Prop) → Prop :=
match n with
| O ⇒ fun k ⇒ ∀ B, k B (fun x1 x2 : B ⇒ x1 = x2)
| S n' ⇒
let k' A B e (f1 f2 : A → B) :=
∀ x1 x2, x1 = x2 → (e (f1 x1) (f2 x2) : Prop) in
fun k ⇒ ∀ A, nary_congruence_statement n' (fun B e ⇒ k _ (k' A B e))
end.
Lemma nary_congruence n (k := fun B e ⇒ ∀ y : B, (e y y : Prop)) :
nary_congruence_statement n k.
Proof.
have: k _ _ := _; rewrite {1}/k.
elim: n k ⇒ [|n IHn] k k_P /= A; first exact: k_P.
by apply: IHn ⇒ B e He; apply: k_P ⇒ f x1 x2 <-.
Qed.
Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal → Plemma → Pgoal.
Proof. by move→. Qed.
Implicit Arguments ssr_congr_arrow [].
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.
Set SsrAstVersion.
Global Set Asymmetric Patterns.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module SsrSyntax.
Reserved Notation "(* x 'is' y 'of' z 'isn't' // /= //= *)" (at level 8).
Reserved Notation "(* 69 *)" (at level 69).
Reserved Notation "(* Use to test if 'SsrSyntax_is_Imported' *)" (at level 8).
Reserved Notation "<hidden n >" (at level 200).
Reserved Notation "T (* n *)" (at level 200, format "T (* n *)").
End SsrSyntax.
Export SsrMatchingSyntax.
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 "x : T" := (x : T)
(at level 100, right associativity,
format "'[hv' x '/ ' : T ']'") : core_scope.
Notation "T : 'Type'" := (T%type : Type)
(at level 100, only parsing) : core_scope.
Notation "P : 'Prop'" := (P%type : Prop)
(at level 100, only parsing) : core_scope.
Definition abstract_lock := unit.
Definition abstract_key := tt.
Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) :=
let: tt := lock in statement.
Notation "<hidden n >" := (abstract _ n _).
Notation "T (* n *)" := (abstract T n abstract_key).
Module TheCanonical.
CoInductive put vT sT (v1 v2 : vT) (s : sT) := 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 & ∀ x : T, P x := T.
Definition dependentReturnType T P & ∀ 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 (p : T) := Phantom.
Implicit Arguments phantom [].
Implicit Arguments Phantom [].
CoInductive phant (p : Type) := Phant.
Definition protect_term (A : Type) (x : A) : A := x.
Notation unkeyed x := (let flex := x in flex).
Definition ssr_converse R (r : R) := (Logic.I, r).
Notation "=^~ r" := (ssr_converse r) (at level 100) : form_scope.
Notation nosimpl t := (let: tt := tt in t).
Lemma master_key : unit. Proof. exact tt. Qed.
Definition locked A := let: tt := master_key in fun x : A ⇒ x.
Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed.
Lemma not_locked_false_eq_true : locked false ≠ true.
Proof. unlock; 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 ].
Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}.
Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed.
Notation "[ 'unlockable' 'of' C ]" := (@Unlockable _ _ C (unlock _))
(at level 0, format "[ 'unlockable' 'of' C ]") : form_scope.
Notation "[ 'unlockable' 'fun' C ]" := (@Unlockable _ (fun _ ⇒ _) C (unlock _))
(at level 0, format "[ 'unlockable' 'fun' C ]") : form_scope.
Definition locked_with k := let: tt := k in fun T x ⇒ x : T.
Lemma locked_withE T k x : unkeyed (locked_with k x) = x :> T.
Proof. by case: k. Qed.
Canonical locked_with_unlockable T k x :=
@Unlockable T x (locked_with k x) (locked_withE k x).
Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T.
Proof. exact: unlock. Qed.
Definition ssr_have Plemma Pgoal (step : Plemma) rest : Pgoal := rest step.
Implicit Arguments ssr_have [Pgoal].
Definition ssr_have_let Pgoal Plemma step
(rest : let x : Plemma := step in Pgoal) : Pgoal := rest.
Implicit Arguments ssr_have_let [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)
: (∀ B, (B → B → Prop) → Prop) → Prop :=
match n with
| O ⇒ fun k ⇒ ∀ B, k B (fun x1 x2 : B ⇒ x1 = x2)
| S n' ⇒
let k' A B e (f1 f2 : A → B) :=
∀ x1 x2, x1 = x2 → (e (f1 x1) (f2 x2) : Prop) in
fun k ⇒ ∀ A, nary_congruence_statement n' (fun B e ⇒ k _ (k' A B e))
end.
Lemma nary_congruence n (k := fun B e ⇒ ∀ y : B, (e y y : Prop)) :
nary_congruence_statement n k.
Proof.
have: k _ _ := _; rewrite {1}/k.
elim: n k ⇒ [|n IHn] k k_P /= A; first exact: k_P.
by apply: IHn ⇒ B e He; apply: k_P ⇒ f x1 x2 <-.
Qed.
Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal → Plemma → Pgoal.
Proof. by move→. Qed.
Implicit Arguments ssr_congr_arrow [].
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.