Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrmatching.

Require Import mathcomp.ssreflect.ssreflect.

Search _ locked.
(*
lock  forall (A : Type) (x : A), x = locked x
not_locked_false_eq_true  locked false <> true
*)

SearchAbout locked.
(*
lock: forall (A : Type) (x : A), x = locked x
not_locked_false_eq_true: locked false <> true
*)

Notation "[ :: x1 , x2 , .. , xn : s ]" := (x1 :: x2 :: .. (xn :: s) ..)
  (at level 0, format
  "'[hv' [ :: '['  x1 , '/'  x2 , '/'  .. , '/'  xn ']' '/ '  :  s ] ']'").

Check fun l => [:: true, false , false : l].

[operator item, item, ..., item short_operator item]

  Inductive wf T : bool -> option T -> Type :=
  | wf_f : wf false None
  | wf_t : forall x, wf true (Some x).

  Derive Inversion wf_inv with (forall T b (o : option T), wf b o) Sort Prop.

  Lemma Problem T b (o : option T) :
    wf b o ->
    match b with
    | true  => exists x, o = Some x
    | false => o = None
    end.
  Proof.
  (* Doesn't work *)
  (* case: b; elim/wf_inv. *)
  case: b; intros top; elim top using wf_inv; clear top.

(* subfilter s : seq sT == when sT has a subType p structure, the sequence    *)
(*                         of items of type sT corresponding to items of s    *)
(*                         for which p holds.                                 *)

Require Import mathcomp.ssreflect.ssreflect.
Require Import Morphisms Setoid.

Section test2.
Context {A} (equiv : relation A) (equiv_equivalence : Equivalence equiv).
Context (P : A -> Prop) (P_Proper : Proper (equiv ==> iff) P).

Lemma test2 x y : equiv x y -> P x -> True.
Proof.
  move=> H1 H2.
  Fail rewrite H1 in H2.
  (* Error: tampering with discharged assumptions of "in" tactical *)
  move: H2; rewrite H1 => H2.
Admitted.
End test2.

# Override COQDEP to find only the "right" copy .ml files
/bin/sh: 1: --no-print-directory: not found

Require Import mathcomp.ssreflect.ssreflect.
Require Import Morphisms Setoid.

Lemma test1 (P : nat -> Prop) x y : P x -> x = y -> True.
Proof.
  intros H1 H2.
  rewrite H2 in H1.
  (* flips the order of H1 and H2 *)
  Restart.
  intros H1 H2.
  rewrite ->H2 in H1.
  (* does not flip the order *)
Admitted.

From mathcomp Require Export ssreflect.

Class Decision (P : Prop) := decide : {P} + {~P}.
Arguments decide _ {_}.
Notation EqDecision A := (forall x y : A, Decision (x = y)).

Global Instance list_eq_dec A {dec : EqDecision A} : EqDecision (list A).
Proof. Admitted.

Section foo.
  Context (iProp: Type) (someP : forall (T:Type), iProp) (op : iProp -> iProp -> iProp) (ent : iProp -> iProp -> Prop).

  Definition PersistentP (P : iProp) := True.
  Existing Class PersistentP.

  Instance someI T `{EqDecision T} : PersistentP (someP T).
  Proof. exact I. Qed.

  Context (lem : forall P Q, PersistentP Q -> (ent P Q) -> ent P (op P Q)).
  Context (P Q : iProp).

  Instance: PersistentP Q | 1000. Proof. exact I. Qed.

  Goal (ent P Q) -> ent P (op P Q).
    intros H. timeout 5 apply: lem. done. (* HERE *)
  Qed. 
End foo.

∀ (M : ucmraT) (P Q : uPred M), PersistentP Q → (P ⊢ Q) → P ⊢ P ∗ Q

<prompt>own_valid_r < 89 |own_valid_r| 0 < </prompt>Set Typeclasses Debug.

<prompt>own_valid_r < 91 |own_valid_r| 0 < </prompt>apply: uPred.always_entails_r.
<infomsg>Debug: 1.1: apply @big_sepS_empty_persistent on (PersistentP ?u0)
</infomsg>

Debug: 1.1: apply @big_sepS_empty_persistent on (PersistentP ?u0)
Debug: 1.1.1.1: apply @fin_dec on (EqDecision ?Goal0)
Debug: 1.1.2.1: apply @finite.finite_countable on (Countable (fin ?Goal1))
Debug: 1.1.2.1.1.1: apply finite.fin_finite on (finite.Finite (fin ?Goal0))
Debug: 1.1: apply @cmra_valid_persistent on (PersistentP (✓ a))

Require Import mathcomp.ssreflect.ssreflect.

Set Primitive Projections.

Record foo A := Foo { foo_car : A }.
Arguments foo_car : simpl never.

Definition bar : foo nat := Foo nat 10.

Goal foo_car _ bar = 10.
unfold foo_car. simpl. (* works. Resulting goal: 10 = 10 *)
Restart.
rewrite /foo_car. (* leaves goal unchanged *) 

diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index a10b9c5..993c0a7 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -22,3 +22,4 @@ ssreflect.ml4

 -I .
 -R . mathcomp.ssreflect
+ssreflect_plugin.mlpack

Require Export Program Setoid Utf8.
Require Export mathcomp.ssreflect.ssreflect.

(* -*- mode: coq; coq-prog-args: ("-emacs" "-Q" "." "" "-top" "cmra") -*- *)
(* File reduced by coq-bug-finder from original input, then from 1113 lines to 184 lines *)

Class Equiv A := equiv: relation A.
Infix "≡" := equiv (at level 70, no associativity).
Notation "(≡)" := equiv (only parsing).
Class Assoc {A} (R : relation A) (f : A → A → A) : Prop :=
  assoc x y z : R (f x (f y z)) (f (f x y) z).

Class Op (A : Type) := op : A → A → A.
Infix "⋅" := op (at level 50, left associativity).
Notation "(⋅)" := op (only parsing).

Structure cmraT := CMRAT {
  cmra_car :> Type;
  cmra_equiv : Equiv cmra_car;
  cmra_op : Op cmra_car;
}.
Existing Instances cmra_op cmra_equiv.

Section cmra.
  Context {A : cmraT}.
  Global Instance cmra_equivalence : Equivalence ((≡) : relation A).
Admitted.
End cmra.


Section cmra_mixin.
  Context {A : cmraT}.
  Global Instance cmra_assoc : Assoc (≡) (@op A _).
Admitted.
End cmra_mixin.
Context {A : cmraT}.
Implicit Types x y z : A.

Lemma L x y z : z ⋅ x ⋅ y ≡ y ⋅ x.
Admitted.

Lemma l x y : x ⋅ y ≡ y ⋅ x.
Proof.
rewrite -L.
rewrite -!assoc.

$ nice make -j5
Generating Makefile.coq for Coq v8.6 with COQBIN=/home/r/bin/coq-8.6/bin/
# Override COQDEP to find only the "right" copy .ml files
COQDEP ssreflect_plugin.mlpack
CAMLDEP -pp ssreflect.ml4
Redundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex].
COQDEP tuple.v
COQDEP prime.v
COQDEP path.v
COQDEP generic_quotient.v
COQDEP fintype.v
COQDEP finset.v
COQDEP fingraph.v
COQDEP finfun.v
COQDEP div.v
COQDEP choice.v
COQDEP binomial.v
COQDEP bigop.v
COQDEP ssrnat.v
COQDEP ssrfun.v
COQDEP ssreflect.v
COQDEP ssrbool.v
COQDEP seq.v
COQDEP eqtype.v
COQDEP all_ssreflect.v
CAMLC -pp -c ssreflect.ml4
Redundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex].
File "ssreflect.ml4", line 675, characters 55-68:
Warning 3: deprecated: Util.String.set
Use Bytes.set instead.
File "ssreflect.ml4", line 755, characters 25-37:
Warning 3: deprecated: Util.String.set
Use Bytes.set instead.
File "ssreflect.ml4", line 756, characters 19-31:
Warning 3: deprecated: Util.String.set
Use Bytes.set instead.
File "ssreflect.ml4", line 756, characters 33-45:
Warning 3: deprecated: Util.String.set
Use Bytes.set instead.
File "ssreflect.ml4", line 757, characters 5-44:
Warning 3: deprecated: Util.String.set
Use Bytes.set instead.
File "ssreflect.ml4", line 1252, characters 10-24:
Warning 3: deprecated: Util.String.set
Use Bytes.set instead.
File "ssreflect.ml4", line 4441, characters 26-123:
Warning 40: this record of type Proofview.Goal.enter contains fields that are 
not visible in the current scope: enter.
They will not be selected if the type becomes unknown.
File "ssreflect.ml4", line 1049, characters 6-9:
Warning 26: unused variable fmt.
File "ssreflect.ml4", line 1053, characters 6-13:
Warning 26: unused variable tacname.
CAMLC -pack -o ssreflect_plugin.cmo
make[1]: *** No rule to make target 'ssreflect_plugin.mllib', needed by 'ssreflect_plugin.cmxa'.  Stop.
Makefile:24: recipe for target 'all' failed
make: *** [all] Error 2

Class C (n : nat) := mkC {}.
(*Instance c : C 3 := mkC _.*)

Goal forall m : nat, (forall n, C n -> m = n) -> m = 3.
Proof.
  move=> m H.
  rewrite H.

Error: The LHS of H
    m
does not match any subterm of the goal

$ coqtop
Welcome to Coq 8.5pl1 (May 2016)

Coq < Require Import mathcomp.algebra.matrix.

Small Scale Reflection version 1.5 loaded.
Copyright 2005-2014 Microsoft Corporation and INRIA.
Distributed under the terms of the CeCILL-B license.

[Loading ML file ssreflect.cmxs ... done]

Small Scale Reflection version 1.5 loaded.
Copyright 2005-2014 Microsoft Corporation and INRIA.
Distributed under the terms of the CeCILL-B license.

[Loading ML file z_syntax_plugin.cmxs ... done]
[Loading ML file quote_plugin.cmxs ... done]
[Loading ML file newring_plugin.cmxs ... done]
Warning: No global reference exists for projection
valuefun
       (x : finfun.finfun_of
              (aT:=fintype.prod_finType
                     (fintype.ordinal_finType _UNBOUND_REL_2)
                     (fintype.ordinal_finType _UNBOUND_REL_1))
              (ssreflect.Phant
                 (fintype.ordinal _UNBOUND_REL_2 *
                  fintype.ordinal _UNBOUND_REL_1 -> _UNBOUND_REL_4)))
       (_ : is_true true) =>
     Matrix (R:=_UNBOUND_REL_5) (m:=_UNBOUND_REL_4) (n:=_UNBOUND_REL_3) x in
instance matrix_subType of eqtype.Sub, ignoring it.

Coq <   

$ opam list| grep coq
coq                     8.5.1  Formal proof management system.
coq-color               1.2.0  A library on rewriting theory and termination.
coq-dpdgraph              0.6  Compute dependencies between Coq objects (definit
coq-ext-lib             0.9.4  A library of Coq definitions, theorems, and tacti
coq-math-classes        1.0.4  A library of abstract interfaces for mathematical
coq-mathcomp-algebra      1.6  Mathematical Components Library on Algebra
coq-mathcomp-fingroup     1.6  Mathematical Components Library on finite groups
coq-mathcomp-ssreflect    1.6  Small Scale Reflection

  rewrite [(a ★ _)%M]lemma.

  rewrite [a ★ _]lemma%M.

Require Import mathcomp.ssreflect.ssreflect Setoid.

Delimit Scope my_scope with M.
Notation "a ★ b" := (a /\ b) (at level 40) : my_scope.

Lemma sep_comm a b : (a ★ b <-> b ★ a)%M.
Proof. tauto. Qed.

Goal forall a b, (a ★ b <-> b ★ a)%M.
Proof.
  move=>a ?.
  (* Need nested parentheses to give a rewrite pattern. *)
  rewrite [(a ★ _)%M]sep_comm.

(* File reduced by coq-bug-finder  *)
Axiom proof_admitted : False.
Tactic Notation "admit" := case proof_admitted.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Unicode.Utf8.

Require Import mathcomp.ssreflect.ssreflect.

Class Equiv A := equiv: relation A.
Infix "≡" := equiv (at level 70, no associativity).
Notation "(≡)" := equiv (only parsing).

Set Primitive Projections.

Class Dist A := dist : nat → relation A.
Notation "x ={ n }= y" := (dist n x y)
  (at level 70, n at next level, format "x  ={ n }=  y").


Record CofeMixin A `{Equiv A, Dist A} := {
  mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ={n}= y;
  mixin_dist_equivalence n : Equivalence (dist n);
  mixin_dist_S n x y : x ={S n}= y → x ={n}= y;
  mixin_dist_0 x y : x ={0}= y;
}.

Structure cofeT := CofeT {
  cofe_car :> Type;
  cofe_equiv : Equiv cofe_car;
  cofe_dist : Dist cofe_car;
  cofe_mixin : CofeMixin cofe_car
}.
Existing Instances cofe_equiv cofe_dist.
Arguments cofe_car : simpl never.

Section cofe_mixin.
  Context {A : cofeT}.
  Implicit Types x y : A.
  Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ={n}= y.
admit.
Defined.
End cofe_mixin.
  Context {A : cofeT}.
  Global Instance cofe_equivalence : Equivalence ((≡) : relation A).
  Proof.
    split.
    *
 intros x. rewrite equiv_dist.

Require Import Arith NPeano.
Require Import mathcomp.ssreflect.ssreflect.

Lemma foo x y z : x <= y -> y <= z -> x <= z.
Proof.
  move=> H1 H2.
  Fail rewrite H1.
  (* Error: not a rewritable relation: (le x y) in rule H1 *)
  rewrite ->H1.
Admitted.

(* File reduced by coq-bug-finder *)
Require Import Coq.Setoids.Setoid.
Require Import Coq.Unicode.Utf8.
Require Import mathcomp.ssreflect.ssreflect.

Global Generalizable All Variables.

Class Lookup (K A M : Type) := lookup: K → M → option A.
Notation "m !! i" := (lookup i m) (at level 20).

Section S1.
Context `{∀ A, Lookup nat A (M A)}.

Definition iProp := Prop.
Definition state := M nat.

Program Definition wp (Q : iProp) : iProp := True.

(* Just some relation. *)
Inductive entails (P Q : Prop) : Prop :=
  | Entails : (P → Q) → entails P Q.

Lemma wp_lift_atomic_step {Q} (φ : state → Prop) :
  entails (False) (wp Q).
Admitted.

Instance uPred_entails_rewrite_relation : RewriteRelation entails.
Global Instance: PreOrder entails.
Proof. Admitted.

Lemma wp_alloc_pst (σ : state) Q :
  entails Q (wp Q).
Proof.
  set (φ σ' := ∃ l, σ' = σ ∧ σ !! l = None).
  rewrite -(wp_lift_atomic_step (λ σ', ∃ l, σ' = σ ∧ σ !! l = None))=>//.

[killy@GLaDOS : ~] which ocamldep
/home/killy/.opam/4.03.0/bin/ocamldep
[killy@GLaDOS : ~] which ocamlc
/home/killy/.opam/4.03.0/bin/ocamlc

Section TEST.

Parameter A: Type.
Parameter world: Type.
Definition prop := world -> Prop.
Parameter wle: world-> world -> Prop.

Goal forall (P:prop) (w w':world), wle w w' -> P w ->
   (forall (w : world), P w -> forall (w' : world), wle w w' -> P w') -> 
    P w'.
Proof.
move => P w w' H_wle HP.
apply.