text:
Set Implicit Arguments.
Set Maximal Implicit Insertion.
Set Contextual Implicit.

From Coq Require Import
     List
     Psatz
     Relation_Definitions
     RelationClasses
     Morphisms
.

Require Import GHC.Base.
Require Import Fix.
Require Import Tactics.Tactics.
Require Import ClassesOfFunctors.FunctorPlus.
Require Import ClassesOfFunctors.AppKleenePlus.
Require Import ClassesOfFunctors.DictDerive.

(** * NetImp

    We first define the NetImp language used to implement the web server shown
    in Fig. 15(a).  *)

Record Connection : Set :=
  MkConn { id : nat ;
           state : nat }.

Definition var : Set -> Set := fun _ => nat.

Inductive exp : Set -> Set :=
| expr {A : Set} : A -> exp A
| avar {A : Set} : var A -> exp (var A)
| deref {A : Set} : var A -> exp A
| proj : nat -> var Connection -> exp nat
| record : exp nat -> exp nat -> exp Connection
| beq : exp nat -> exp nat -> exp bool
| not : exp bool -> exp bool.

Inductive ev : Set -> Set :=
| accept : ev nat
| read : exp nat -> ev nat
| write : exp nat -> exp nat -> ev nat.

Inductive command : Set :=
| Assign {A : Set} : exp (var A) -> exp A -> command
| Run : exp (var nat) -> ev nat -> command
| LAdd : var Connection -> var (list (var Connection)) -> command
| UpdateProj : nat -> exp (var Connection) -> exp nat -> command
| Seq : command -> command -> command
| If : exp bool -> command -> command -> command
| For : var (var Connection) -> var (list (var Connection)) -> command -> command
| Skip : command.

Definition idP := 0.
Definition stateP := 1.

Notation "v ::= e" := (Assign v e) (at level 42).
Notation "v ::<- e" := (Run v e) (at level 42).
Notation "v ::++ e" := (LAdd v e) (at level 42).
Notation "v '::=id' e" := (UpdateProj idP v e) (at level 42).
Notation "v '::=state' e" := (UpdateProj stateP v e) (at level 42).
Notation "c1 ;; c2" := (Seq c1 c2) (at level 43, right associativity).
Notation "'IFB' b 'THEN' c 'END'" := (If b c Skip) (at level 44).
Notation "'IFB' b 'THEN' c1 'ELSE' c2 'END'" := (If b c1 c2) (at level 44).
Notation "'FOR' x 'IN' y 'DO' c 'END'" := (For x y c) (at level 45).

(* local variables *)
Definition y : var (var Connection) := 1.
Definition r : var nat := 5.
Definition newconn : var nat := 10.
Definition newconn_rec : var Connection := 15.

(* global variables *)
Definition s : var nat := 20.
Definition conns : var (list (var Connection)) := 21.

Definition State := nat.
Definition READING := 0.
Definition WRITING := 1.
Definition CLOSED := 2.

(** * A test program. *)
Definition process_test : command :=
  avar s ::= expr 0 ;;
  avar newconn ::<- accept.

(** * The Implementation.

    This is the one shown in Fig. 15(a). *)

Definition process : command :=
  avar newconn ::<- accept ;;
  IFB (not (beq (deref newconn) (expr 0))) THEN
      avar newconn_rec ::= record (deref newconn) (expr READING) ;;
      conns ::++ newconn_rec
  END ;;
  FOR y IN conns DO
      IFB (beq (proj stateP y) (expr WRITING)) THEN
          avar r ::<- write (proj idP y) (deref s) ;;
          deref y ::=state expr CLOSED
      END ;;
      IFB (beq (proj stateP y) (expr READING)) THEN
          avar r ::<- read (proj idP y) ;;
          IFB (beq (deref r) (expr 0)) THEN
              deref y ::=state expr CLOSED
          ELSE
               avar s ::= deref r ;;
               deref y ::=state expr WRITING
          END
      END
  END.

(** * Effects *)

Variant NetworkEff (K : Set -> Set) : Set -> Set :=
| AcceptE : NetworkEff K nat
| ReadE : nat -> NetworkEff K nat
| WriteE : nat -> nat -> NetworkEff K nat.

Arguments AcceptE {_}.
Arguments ReadE {_}.
Arguments WriteE {_}.

Variant MemoryEff (K : Set -> Set) : Set -> Set :=
| SetE {A : Set} : var A -> A -> MemoryEff K unit
| GetE {A : Set}: var A -> MemoryEff K A.

Arguments SetE {_} {_}.
Arguments GetE {_} {_}.

Variant FailEff (K : Set -> Set) : Set -> Set :=
| ErrorE {A : Set} : FailEff K A.

Arguments ErrorE {_} {_}.

Definition fmap1_NetWorkEff {F G : Set -> Set} {A : Set}
           (f : forall X, F X -> G X)
           (a : NetworkEff F A) : NetworkEff G A :=
  match a with
  | AcceptE => AcceptE
  | ReadE c => ReadE c
  | WriteE c n => WriteE c n
  end.

#[global] Program Instance Functor1__NetworkEff : Functor1 NetworkEff :=
  {| fmap1 := @fmap1_NetWorkEff |}.
Next Obligation.
  intros x; destruct x; reflexivity.
Qed.
Next Obligation.
  intros x; destruct x; reflexivity.
Qed.

Definition fmap1_MemoryEff {F G : Set -> Set} {A : Set}
           (f : forall X, F X -> G X)
           (a : MemoryEff F A) : MemoryEff G A :=
  match a with
  | SetE variable va => SetE variable va
  | GetE variable => GetE variable
  end.

#[global] Program Instance Functor1__MemoryEff : Functor1 MemoryEff :=
  {| fmap1 := @fmap1_MemoryEff |}.
Next Obligation.
  intros x; destruct x; reflexivity.
Qed.
Next Obligation.
  intros x; destruct x; reflexivity.
Qed.

Definition fmap1_FailEff {F G : Set -> Set} {A : Set}
           (f : forall X, F X -> G X)
           (a : FailEff F A) : FailEff G A :=
  match a with
  | ErrorE => ErrorE
  end.

#[global] Program Instance Functor1__FailEff : Functor1 FailEff :=
  {| fmap1 := @fmap1_FailEff |}.
Next Obligation.
  intros x; destruct x; reflexivity.
Qed.
Next Obligation.
  intros x; destruct x; reflexivity.
Qed.

(** Smart constructors for effects. *)
Section SmartConstructors.

  Variable F : (Set -> Set) -> Set -> Set.
  Context `{Functor1 F}.

  Section NetworkConstructors.

    Context `{NetworkEff -≪ F}.

    Definition acceptE : Fix1 F nat :=
      @inF1 _ _ _ (inj1 AcceptE).

    Definition readE (conn : nat) : Fix1 F nat :=
      @inF1 _ _ _ (inj1 (ReadE conn)).

    Definition writeE (conn : nat) (val : nat) : Fix1 F nat :=
      @inF1 _ _ _ (inj1 (WriteE conn val)).

  End NetworkConstructors.

  Section MemoryConstructors.

    Context `{MemoryEff -≪ F}.
    Variable A : Set.

    Definition setE (v : var A) (val : A) : Fix1 F unit :=
      @inF1 _ _ _ (inj1 (SetE v val)).

    Definition getE (v : var A) : Fix1 F A :=
      @inF1 _ _ _ (inj1 (GetE v)).

  End MemoryConstructors.

  Section FailConstructors.

    Context `{FailEff -≪ F}.
    Variable A : Set.

    Definition errorE : Fix1 F A :=
      @inF1 _ _ _ (inj1 ErrorE).

  End FailConstructors.

End SmartConstructors.

(** * Program Adverbs. *)

Require Import Adverb.Composable.Purely.
Require Import Adverb.Composable.Dynamically.

Definition LanAdverbs := PurelyAdv ⊕ DynamicallyAdv ⊕
                                   NetworkEff ⊕ MemoryEff ⊕ FailEff.

Definition Lan : Set -> Set := Fix1 LanAdverbs.

Definition getProj (n : nat) (c : Connection) : Lan nat :=
  if (Nat.eqb n idP) then
    pure (id c)
  else if (Nat.eqb n stateP) then
         pure (state c)
       else @errorE _ _ _ _.

(** Denoting [exp] using [Lan]. *)
Fixpoint denote_exp {A : Set} (e : exp A) : Lan A.
  destruct e.
  - exact (pure a).
  - exact (pure v).
  - exact (@getE _ _ _ _ v).
  - exact (@getE _ _ _ _ v >>= getProj n).
  - exact (@denote_exp _ e1 >>=
                       (fun val1 =>
                          @denote_exp _ e2 >>=
                                      (fun val2 => pure (MkConn val1 val2)))).
  - exact (@denote_exp _ e1 >>=
                       (fun val1 =>
                          @denote_exp _ e2 >>=
                                      (fun val2 => pure (Nat.eqb val1 val2)))).
  - exact (fmap negb (@denote_exp _ e)).
Defined.

(** Denoting [av] using [Lan]. *)
Definition denote_ev {A : Set} (e : ev A) : Lan nat :=
  match e with
  | accept => @acceptE _ _ _
  | read e => @denote_exp _ e >>= @readE _ _ _
  | write c e => @denote_exp _ c >>= (fun conn =>
                   (@denote_exp _ e >>= @writeE _ _ _ conn))
  end.

(** Denoting [command] using [Lan]. *)
Fixpoint denote_command (c : command) : Lan unit.
  destruct c.
  - (* Assign *)
    refine (@denote_exp _ e >>=
                            (fun v => @denote_exp _ e0 >>= _)).
    exact (@setE _ _ _ _ v).
  - (* Run *)
    exact (@denote_exp _ e >>=
               (fun v => @denote_ev _ e0 >>= @setE _ _ _ _ v)).
  - (* LAdd *)
    refine (@getE _ _ _ _ v0 >>= _).
    refine (fun xs => @setE _ _ _ _ v0 (v :: xs)).
  - (* UpdateProj *)
    refine (@denote_exp _ e >>= (fun v => _)).
    refine (@getE _ _ _ _ v >>=
                  (fun c => @denote_exp _ e >>= (fun val => _))).
    exact (if (Nat.eqb n idP) then
              @setE _ _ _ _ v (MkConn val (state c))
            else if (Nat.eqb n stateP) then
                   @setE _ _ _ _ v (MkConn (id c) val)
                 else @errorE _ _ _ _).
  - (* Seq *)
    exact (denote_command c1 >> denote_command c2).
  - (* If *)
    exact (@denote_exp _ e >>= (fun b => if b then denote_command c1
                                      else denote_command c2)).
  - (* For *)
    refine (@getE _ _ _ _ v0 >>= (fun xs => _)).
    (** The loop variable is a pointer. *)
    pose (@mapM _ _ _ Functor__DynamicallyAdv
                Applicative__DynamicallyAdv
                Monad__DynamicallyAdv (fun v' =>
                   @setE _ _ _ _ v v' >> denote_command c) xs).
    exact (fmap (fun _ => tt) f).
  - (* Skip *)
    exact (pure tt).
Defined.

(** * Adverb Theories. *)

Require Import Eq.EqEq.
Require Import Eq.EqBindLaws.
Require Import Eq.EqBindK.
Require Import Eq.EqBindCong.

Unset Implicit Arguments.

Definition EqRel (D : (Set -> Set) -> Set -> Set)
           `{PurelyAdv -≪ D} `{DynamicallyAdv -≪ D} `{Functor1 D}
  := EqEq (F:=Fix1 D) ⊎ EqBindLaws ⊎ EqBindCong.

Set Implicit Arguments.

Definition EqLanRel := EqRel LanAdverbs.

Definition EqLan := FixRel EqLanRel.

#[global] Instance Equivalence_EqLan {A : Set} : Equivalence (@EqLan A).
typeclasses eauto.
Qed.

(** A test program written in adverbs. *)
Definition process_testEmbedded : Lan unit :=
  @setE _ _ _ _ s 0 >>
  @acceptE _ _ _ >>= (fun val =>
  @setE _ _ _ _ newconn val).

(** * Custom tactics. *)
(* In the case that the part before [>>=] are equal, we move on *)
Ltac forward :=
  apply eqBindCong; [reflexivity|intros].

Ltac simplify_rets :=
  repeat (rewrite ?(@PureRet LanAdverbs _ _ _),
      ?(@eqBindLeftId LanAdverbs _ _ _ EqLanRel _ _ _ _)).

(** * A test.

    We show that denoting [process_test] into [Lan] gives us
    [process_testEmbedded].  *)

Goal EqLan (@denote_command process_test) (@process_testEmbedded).
Proof.
  unfold process_test, process_testEmbedded.
  unfold denote_command, denote_exp.
  assert (forall (a b : Lan unit) , (a >> b) = (a >>= (fun _ => b)))
    by reflexivity.
  rewrite !H.
  simplify_rets. unfold denote_exp.
  simplify_rets. forward.
  simplify_rets. unfold denote_ev, "∘". reflexivity.
Qed.

(** * The specification language.

    We only refine the commands. We reuse [exp] and [ev] from NetImp. *)

Inductive commandS : Set :=
| AssignS {A : Set} : exp (var A) -> exp A -> commandS
| RunS : exp (var nat) -> ev nat -> commandS
| LAddS : var Connection -> var (list (var Connection)) -> commandS
| UpdateProjS : nat -> exp (var Connection) -> exp nat -> commandS
| SeqS : commandS -> commandS -> commandS
| IfS : exp bool -> commandS -> commandS -> commandS
| SomeS : commandS -> commandS
| OrS : commandS -> commandS -> commandS
| OneOfS : var (list (var Connection)) ->
           var (var Connection) -> commandS -> commandS
| SkipS : commandS.

Declare Scope spec_scope.

Notation "v ::= e" := (AssignS v e) (at level 42) : spec_scope.
Notation "v ::<- e" := (RunS v e) (at level 42) : spec_scope.
Notation "v ::++ e" := (LAddS v e) (at level 42) : spec_scope.
Notation "v '::=id' e" := (UpdateProjS idP v e) (at level 42) : spec_scope.
Notation "v '::=state' e" := (UpdateProjS stateP v e) (at level 42) : spec_scope.
Notation "c1 ;; c2" := (SeqS c1 c2) (at level 43, right associativity) : spec_scope.
Notation "'IFB' b 'THEN' c 'END'" := (IfS b c SkipS) (at level 44) : spec_scope.
Notation "'IFB' b 'THEN' c1 'ELSE' c2 'END'" := (IfS b c1 c2) (at level 44) : spec_scope.

Open Scope spec_scope.
Delimit Scope spec_scope with spec.

(** * The specification. *)

Definition processSpec' : commandS :=
  OrS (avar newconn ::<- accept ;;
      IFB (not (beq (deref newconn) (expr 0))) THEN
          avar newconn_rec ::= record (deref newconn) (expr READING) ;;
          conns ::++ newconn_rec
      END)
     (OneOfS (conns) y (
          OrS (IFB (beq (proj stateP y) (expr WRITING)) THEN
                  avar r ::<- write (proj idP y) (deref s) ;;
                  deref y ::=state expr CLOSED
              END)
             (IFB (beq (proj stateP y) (expr READING)) THEN
                  avar r ::<- read (proj idP y) ;;
                  IFB (beq (deref r) (expr 0)) THEN
                      deref y ::=state expr CLOSED
                  ELSE
                       avar s ::= deref r ;;
                       deref y ::=state expr WRITING
                  END
                  END))).

Definition processSpec := SomeS processSpec'.

(** * Adverbs for the specification language.

    We need a few additional adverbs for embedding the specification
    language. *)

Require Import Adverb.Composable.Nondeterministically.
Require Import Adverb.Composable.Repeatedly.

Definition SpecAdverbs := ReifiedKleenePlus ⊕ ReifiedPlus ⊕ LanAdverbs.

Definition Spec : Set -> Set := Fix1 SpecAdverbs.

Definition lanToSpec {A : Set} (l : Lan A) : Spec A :=
  foldFix1 (fun _ s => @inF1 _ _ _ (inj1 s)) l.

Definition getProjS (n : nat) (c : Connection) : Spec nat :=
  if (Nat.eqb n idP) then
    pure (id c)
  else if (Nat.eqb n stateP) then
         pure (state c)
       else @errorE _ _ _ _.

(** Re-denote [exp] and [ev] using the [Spec] adverb. *)

Fixpoint denote_expS {A : Set} (e : exp A) : Spec A.
  destruct e.
  - exact (pure a).
  - exact (pure v).
  - exact (@getE _ _ _ _ v).
  - exact (@getE _ _ _ _ v >>= getProjS n).
  - exact (@denote_expS _ e1 >>=
                       (fun val1 =>
                          @denote_expS _ e2 >>=
                                      (fun val2 => pure (MkConn val1 val2)))).
  - exact (@denote_expS _ e1 >>=
                       (fun val1 =>
                          @denote_expS _ e2 >>=
                                      (fun val2 => pure (Nat.eqb val1 val2)))).
  - exact (fmap negb (@denote_expS _ e)).
Defined.

Definition denote_evS {A : Set} (e : ev A) : Spec nat :=
  match e with
  | accept => @acceptE _ _ _
  | read e => @denote_expS _ e >>= @readE _ _ _
  | write c e => @denote_expS _ c >>= (fun conn =>
                   (@denote_expS _ e >>= @writeE _ _ _ conn))
  end.

(** Denoting [command]. *)

Fixpoint denote_command' (c : command) : Spec unit.
  destruct c.
  - (* Assign *)
    refine (@denote_expS _ e >>=
                            (fun v => @denote_expS _ e0 >>= _)).
    exact (@setE _ _ _ _ v).
  - (* Run *)
    exact (@denote_expS _ e >>=
               (fun v => @denote_evS _ e0 >>= @setE _ _ _ _ v)).
  - (* LAdd *)
    refine (@getE _ _ _ _ v0 >>= _).
    refine (fun xs => @setE _ _ _ _ v0 (v :: xs)).
  - (* UpdateProj *)
    refine (@denote_expS _ e >>= (fun v => _)).
    refine (@getE _ _ _ _ v >>=
                  (fun c => @denote_expS _ e >>= (fun val => _))).
    exact (if (Nat.eqb n idP) then
              @setE _ _ _ _ v (MkConn val (state c))
            else if (Nat.eqb n stateP) then
                   @setE _ _ _ _ v (MkConn (id c) val)
                 else @errorE _ _ _ _).
  - (* Seq *)
    exact (denote_command' c1 >> denote_command' c2).
  - (* If *)
    exact (@denote_expS _ e >>= (fun b => if b then denote_command' c1
                                      else denote_command' c2)).
  - (* For *)
    refine (@getE _ _ _ _ v0 >>= (fun xs => _)).
    (** The loop variable is a pointer. *)
    refine (foldr (fun vc s => @setE _ _ _ _ v vc >>
                                  denote_command' c >> s)
                  (pure tt) xs).
  - (* Skip *)
    exact (pure tt).
Defined.

(** Denoting [commandS]. *)

Fixpoint denote_command_Spec (c : commandS) : Spec unit.
  destruct c.
  - (* Assign *)
    refine (@denote_expS _ e >>=
                            (fun v => @denote_expS _ e0 >>= _)).
    exact (@setE _ _ _ _ v).
  - (* Run *)
    exact (@denote_expS _ e >>=
               (fun v => @denote_evS _ e0 >>= @setE _ _ _ _ v)).
  - (* LAdd *)
    refine (@getE _ _ _ _ v0 >>= _).
    refine (fun xs => @setE _ _ _ _ v0 (v :: xs)).
  - (* UpdateProj *)
    refine (@denote_expS _ e >>= (fun v => _)).
    refine (@getE _ _ _ _ v >>=
                  (fun c => @denote_expS _ e >>= (fun val => _))).
    exact (if (Nat.eqb n idP) then
              @setE _ _ _ _ v (MkConn val (state c))
            else if (Nat.eqb n stateP) then
                   @setE _ _ _ _ v (MkConn (id c) val)
                 else @errorE _ _ _ _).
  - (* Seq *)
    exact (denote_command_Spec c1 >> denote_command_Spec c2).
  - (* If *)
    exact (@denote_expS _ e >>= (fun b => if b then denote_command_Spec c1
                                           else denote_command_Spec c2)).
  - (* Some *)
    exact (@kleenePlus _ _ _ _ _ (denote_command_Spec c)).
  - (* Or *)
    exact (@kleenePlus _ _ _ _ _ (fplus (denote_command_Spec c1) (denote_command_Spec c2))).
  - (* OneOf *)
    refine (@getE _ _ _ _ v >>= (fun xs => _)).
    refine (@kleenePlus _ _ _ _ _
                        (foldr (fun vc s => fplus (@setE _ _ _ _ v0 vc >>
                                                (denote_command_Spec c)) s)
                               (pure tt) xs)).
  - (* Skip *)
    exact (pure tt).
Defined.

(** * The theories for the [Spec] adverb. *)

Require Import Eq.EqChoiceLaws.

Definition EqSpecRel := EqFplusLaws ⊎ (EqRel SpecAdverbs).

Definition EqSpec := FixRel EqSpecRel.

#[global] Instance Equivalence_EqSpec {A : Set} : Equivalence (@EqSpec A).
typeclasses eauto.
Qed.

Require Import Refines.RefinesEq.
Require Import Refines.RefinesOrder.
Require Import Refines.RefinesChoice.
Require Import Refines.RefinesStar.

Definition RefinesRel := RefinesEq (@EqSpec) _ ⊎ RefinesOrder ⊎
                                   RefinesFplusLaws ⊎ RefinesKleenePlusLaws ⊎
                                   EqBindCong.

Definition refines := FixRel RefinesRel.

#[global] Instance PreOrder_RefinesRel {A : Set} : PreOrder (@refines A).
typeclasses eauto.
Qed.

Notation "a ⊆ b" := (refines a b) (at level 50).

Close Scope spec_scope.

(** * The refinement proofs. *)

(** Our refinement proofs work as follow: we first abstract the program as three
    fragments. *)

Definition fragmentA : command :=
  avar newconn ::<- accept ;;
  IFB (not (beq (deref newconn) (expr 0))) THEN
      avar newconn_rec ::= record (deref newconn) (expr READING) ;;
      conns ::++ newconn_rec
  END.

Definition fragmentB : command :=
  IFB (beq (proj stateP y) (expr WRITING)) THEN
    avar r ::<- write (proj idP y) (deref s) ;;
    deref y ::=state expr CLOSED
  END.

Definition fragmentC : command :=
  IFB (beq (proj stateP y) (expr READING)) THEN
    avar r ::<- read (proj idP y) ;;
    IFB (beq (deref r) (expr 0)) THEN
      deref y ::=state expr CLOSED
    ELSE
      avar s ::= deref r ;;
      deref y ::=state expr WRITING
    END
  END.

(** Now we prove that our implementation refines our specification by
    layers. Here is the first layer: *)

(** * The first layer. *)

Definition process_l1 :=
  fragmentA ;;
  FOR y IN conns DO
      fragmentB ;;
      fragmentC
  END.

Global Instance CongProper {A : Set}
       `{forall (A : Set), Equivalence (FixRel EqSpecRel A)} :
  Proper (FixRel EqSpecRel A ==>
          FixRel EqSpecRel A ==>
          iff) (FixRel EqSpecRel A).
typeclasses eauto.
Defined.

(** We show that [process] refines [process_l1]. *)

Lemma refinesL1 :
  (@denote_command' process) ⊆ (@denote_command' process_l1).
Proof.
  apply (@refinesEq _ _ (@EqSpec) _ _ _).
  unfold process, process_l1, fragmentA, fragmentB, fragmentC.
  unfold denote_command', denote_command_Spec, denote_expS.
  assert (forall (a b : Spec unit) , (a >> b) = (a >>= (fun _ => b)))
    by reflexivity.
  assert (forall {A B : Set} (f : A -> B)(a : Spec A),
             fmap f a = (a >>= (fun a => return_ (f a))))
    by reflexivity.
  rewrite !(@PureRet SpecAdverbs _ _ _).
  rewrite !H, !H0.
  rewrite !(@eqBindAssoc SpecAdverbs _ _ _ EqSpecRel _ _).
  rewrite !(@eqBindAssoc SpecAdverbs _ _ _ EqSpecRel _ _ _ _ _ (return_ newconn)).
  repeat forward.
  rewrite !(@eqBindAssoc SpecAdverbs _ _ _ EqSpecRel _ _ _ _ _ (@denote_evS nat accept >>= setE a)).
  reflexivity.
Qed.

(** Similarly, we also divide the specification into three fragments. *)

Open Scope spec_scope.

Definition fragmentAS : commandS :=
  avar newconn ::<- accept ;;
  IFB (not (beq (deref newconn) (expr 0))) THEN
      avar newconn_rec ::= record (deref newconn) (expr READING) ;;
      conns ::++ newconn_rec
  END.

Definition fragmentBS : commandS :=
  IFB (beq (proj stateP y) (expr WRITING)) THEN
    avar r ::<- write (proj idP y) (deref s) ;;
    deref y ::=state expr CLOSED
  END.

Definition fragmentCS : commandS :=
  IFB (beq (proj stateP y) (expr READING)) THEN
    avar r ::<- read (proj idP y) ;;
    IFB (beq (deref r) (expr 0)) THEN
      deref y ::=state expr CLOSED
    ELSE
      avar s ::= deref r ;;
      deref y ::=state expr WRITING
    END
    END.

(** We show that each fragment of the implementation refines a fragment of the
    specification. *)

Lemma fragmentA_refines :
  (@denote_command' fragmentA) ⊆ (@denote_command_Spec fragmentAS).
Proof. reflexivity. Qed.

Lemma fragmentB_refines :
  (@denote_command' fragmentB) ⊆ (@denote_command_Spec fragmentBS).
Proof. reflexivity. Qed.

Lemma fragmentC_refines :
  (@denote_command' fragmentC) ⊆ (@denote_command_Spec fragmentCS).
Proof. reflexivity. Qed.

Opaque fragmentA.
Opaque fragmentB.
Opaque fragmentC.
Opaque fragmentAS.
Opaque fragmentBS.
Opaque fragmentCS.

(** * The second layer. *)

Definition process_l2 :=
  fragmentAS ;;
  OneOfS conns y
         (fragmentBS ;; fragmentCS).

Opaque fplus.
Opaque kleenePlus.

Open Scope nat_scope.

Lemma refinesL2 :
  (@denote_command' process_l1) ⊆ (@denote_command_Spec process_l2).
Proof.
  cbn. repeat forward.
  etransitivity.
  2: { apply (@refinesSeq SpecAdverbs _ _ _ _ _ (@RefinesRel) _ _) with (n:=(length a0)).
       reflexivity.
  }
  induction a0.
  - reflexivity.
  - cbn. etransitivity.
    + apply (@refinesEq _ _ (@EqSpec) _ _ _). symmetry.
      apply (@eqBindAssoc SpecAdverbs _ _ _ EqSpecRel _ _).
    + apply eqBindCong.
      * apply (@refinesFplusL SpecAdverbs _ _ _ (@RefinesRel) _ _).
      * intros []. etransitivity.
        -- apply IHa0.
        -- remember (foldr
          (fun (vc : var Connection) (s0 : Fix1 SpecAdverbs unit) =>
           fplus
             (bind_fm (@setE SpecAdverbs Functor1__SumE Inj1_Sum1_r (var Connection) y vc)
                (fun _ : unit =>
                 bind_fm (@denote_command_Spec fragmentBS) (fun _ : unit => @denote_command_Spec fragmentCS))) s0)
          (return_fm tt) a1) as x. clear IHa0. clear Heqx.
          induction a1.
           ++ cbn. apply (@refinesFplusR SpecAdverbs _ _ _ (@RefinesRel) _ _).
           ++ cbn. apply eqBindCong.
              ** apply (@refinesFplusR SpecAdverbs _ _ _ (@RefinesRel) _ _).
              ** intros []. apply IHa1.
Qed.

(** * The third layer. *)

Definition process_l3 :=
  fragmentAS ;;
  OneOfS conns y
         (OrS fragmentBS fragmentCS).

Lemma refinesL3 :
  (@denote_command_Spec process_l2) ⊆ (@denote_command_Spec process_l3).
Proof.
  cbn. repeat forward.
  apply refinesKleenePlus.
  induction a0.
  - cbn. replace (return_fm tt) with (@seq SpecAdverbs _ _ _ _ (return_fm tt) 0).
    + apply refinesSeq; reflexivity.
    + reflexivity.
  - cbn. apply refinesFplus.
    + etransitivity.
      * Unshelve.
         2: {
           exact (bind_fm
                    (@setE SpecAdverbs Functor1__SumE Inj1_Sum1_r (var Connection) y a0)
                    (fun _ : unit => bind_fm
                                    (fplus (@denote_command_Spec fragmentBS) (@denote_command_Spec fragmentCS))
                                    (fun _ : unit => (fplus (@denote_command_Spec fragmentBS) (@denote_command_Spec fragmentCS))))).
         }
         repeat forward. apply eqBindCong.
        -- apply refinesFplusL.
        -- intros. apply refinesFplusR.
      * etransitivity.
        -- Unshelve.
           2: {
             exact ((bind_fm (@setE SpecAdverbs Functor1__SumE Inj1_Sum1_r (var Connection) y a0)
                             (fun _ : unit => kleenePlus (fplus (@denote_command_Spec fragmentBS) (@denote_command_Spec fragmentCS))))).
           }
           repeat forward.
           replace ((bind_fm (fplus (@denote_command_Spec fragmentBS) (@denote_command_Spec fragmentCS))
                             (fun _ : unit => fplus (@denote_command_Spec fragmentBS) (@denote_command_Spec fragmentCS))))
             with (@seq SpecAdverbs _ _ _ _ (fplus (@denote_command_Spec fragmentBS) (@denote_command_Spec fragmentCS)) 1) by reflexivity.
           apply refinesSeq; reflexivity.
        -- replace ((bind_fm (@setE SpecAdverbs Functor1__SumE Inj1_Sum1_r (var Connection) y a0)
                             (fun _ : unit => kleenePlus (fplus (@denote_command_Spec fragmentBS) (@denote_command_Spec fragmentCS)))))
             with (@seq SpecAdverbs _ _ _ _ (bind_fm (@setE SpecAdverbs Functor1__SumE Inj1_Sum1_r (var Connection) y a0)
                                                     (fun _ : unit => kleenePlus (fplus (@denote_command_Spec fragmentBS) (@denote_command_Spec fragmentCS)))) 0) by reflexivity.
           apply refinesSeq, refinesFplusL.
    + replace (foldr (fun (vc : var Connection) (s0 : Fix1 SpecAdverbs unit) =>
        fplus
          (bind_fm (@setE SpecAdverbs Functor1__SumE Inj1_Sum1_r (var Connection) y vc)
             (fun _ : unit => bind_fm (@denote_command_Spec fragmentBS) (fun _ : unit => @denote_command_Spec fragmentCS)))
          s0) (return_fm tt) a1) with
          (@seq SpecAdverbs _ _ _ _ (foldr (fun (vc : var Connection) (s0 : Fix1 SpecAdverbs unit) =>
        fplus
          (bind_fm (@setE SpecAdverbs Functor1__SumE Inj1_Sum1_r (var Connection) y vc)
             (fun _ : unit => bind_fm (@denote_command_Spec fragmentBS) (fun _ : unit => @denote_command_Spec fragmentCS)))
          s0) (return_fm tt) a1) 0) by reflexivity.
      etransitivity. exact IHa0.
      eapply refinesKleenePlusCong.
      apply refinesFplusR.
Qed.

(** * The fourth layer. *)

Definition process_l4 :=
  SomeS (OrS fragmentAS (OneOfS conns y (OrS fragmentBS fragmentCS))).

Lemma refinesL4 :
  (@denote_command_Spec process_l3) ⊆ (@denote_command_Spec process_l4).
Proof.
  cbn.
  etransitivity.
  2: { apply (@refinesSeq SpecAdverbs _ _ _ _ _ (@RefinesRel) _ _) with (n:=1).
       reflexivity.
  }
  cbn. eapply eqBindCong.
  - replace (@denote_command_Spec fragmentAS)
      with (@seq SpecAdverbs _ _ _ _ (@denote_command_Spec fragmentAS) 0) by reflexivity.
    apply refinesSeq, refinesFplusL.
  - intros [].
    replace ((bind_fm (@getE SpecAdverbs Functor1__SumE Inj1_Sum1_r (list (var Connection)) conns)
       (fun xs : list (var Connection) =>
        kleenePlus
          (foldr
             (fun (vc : var Connection) (s0 : Fix1 SpecAdverbs unit) =>
              fplus
                (bind_fm (@setE SpecAdverbs Functor1__SumE Inj1_Sum1_r (var Connection) y vc)
                   (fun _ : unit =>
                    kleenePlus (fplus (@denote_command_Spec fragmentBS) (@denote_command_Spec fragmentCS)))) s0)
             (return_fm tt) xs))))
      with (@seq SpecAdverbs _ _ _ _ (bind_fm (@getE SpecAdverbs Functor1__SumE Inj1_Sum1_r (list (var Connection)) conns)
       (fun xs : list (var Connection) =>
        kleenePlus
          (foldr
             (fun (vc : var Connection) (s0 : Fix1 SpecAdverbs unit) =>
              fplus
                (bind_fm (@setE SpecAdverbs Functor1__SumE Inj1_Sum1_r (var Connection) y vc)
                   (fun _ : unit =>
                    kleenePlus (fplus (@denote_command_Spec fragmentBS) (@denote_command_Spec fragmentCS)))) s0)
             (return_fm tt) xs))) 0) by reflexivity.
    apply refinesSeq, refinesFplusR.
Qed.

(** The fourth layer is the spec. *)

Lemma fourth_is_spec :
  process_l4 = processSpec.
Proof. reflexivity. Qed.

author: lastland

repo: ProgramAdverbs


Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Specific.montgomery64_2e224m2e96p1_4limbs.Synthesis.

(* TODO : change this to field once field isomorphism happens *)
Definition sub :
  { sub : feBW_small -> feBW_small -> feBW_small
  | forall a b, phiM_small (sub a b) = F.sub (phiM_small a) (phiM_small b) }.
Proof.
  Set Ltac Profiling.
  Time synthesize_sub ().
  Show Ltac Profile.
Time Defined.

Print Assumptions sub.


text:
Require Export msl.Axioms.

(*** NO AXIOMS AFTER THIS POINT ******************)

Require Import EqdepFacts.

(* From EqdepTh we obtain inj_pair and inj_pairT2 without
   use of excluded middle:
 *)
Module EqdepElim: EqdepElimination.
Lemma eq_rect_eq :
    forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p),
      x = eq_rect p Q x p h.
Proof.
  intros.
  apply Streicher_K__eq_rect_eq.
  apply UIP_refl__Streicher_K.
  unfold UIP_refl_.
  intros.
  apply proof_irr.
Qed.
End EqdepElim.

Module EqdepTh := EqdepTheory EqdepElim.
Export EqdepTh.

(* Generalize the extensionality tactic from the Coq library. *)
Tactic Notation "extensionality" :=
 let x := fresh "x" in extensionality x.

Tactic Notation "extensionality" ident(x) ident(y) :=
    extensionality x; extensionality y.

Tactic Notation "extensionality" ident(x) ident(y) ident(z):=
    extensionality x; extensionality y z.

Lemma imp_ext: forall (A A' B B' : Prop), (A=A') -> (A -> (B=B')) -> ((A->B)=(A'->B')).
Proof.
intros.
subst A'.
apply prop_ext; split; intros; auto.
rewrite <- H0; auto. rewrite H0; auto.
Qed.

Lemma exists_ext: forall (A: Type) F G, (forall x: A, F x = G x) -> (Logic.ex F = Logic.ex G).
Proof.
intros.
apply prop_ext; split; intro; destruct H0; exists x.
rewrite <- H; auto.
rewrite H; auto.
Qed.

Lemma and_ext: forall A B C D, A=B -> C=D -> (A /\ C) = (B /\ D).
Proof.
intros.
rewrite H; rewrite H0; auto.
Qed.

Lemma and_ext': forall (A: Prop) B C D, A=B -> (A -> (C=D)) -> (A /\ C) = (B /\ D).
Proof.
intros.
subst B.
apply prop_ext.
intuition; subst; auto.
Qed.

Lemma or_ext: forall A B C D, A=B -> C=D -> (A \/ C) = (B \/ D).
Proof.
intros.
rewrite H; rewrite H0; auto.
Qed.

Lemma forall_ext: forall (A: Type) (F: A -> Prop) G, (forall x:A, F x = G x) -> (forall x, F x) = (forall x, G x).
Proof.
intros.
apply prop_ext. split; intros. rewrite <- H; auto. rewrite H; auto.
Qed.

Lemma existT_ext:
  forall (A: Type) (P: A -> Prop) (x y: A) (Hx: P x) (Hy: P y),
     x = y -> existT _ x Hx = existT _ y Hy.
Proof.
intros.
subst.
rewrite (proof_irr Hx Hy); auto.
Qed.

Lemma exist_ext:
  forall (A: Type) (P: A -> Prop) (x y: A) (Hx: P x) (Hy: P y),
     x = y -> exist _ x Hx = exist _ y Hy.
Proof.
intros.
subst.
rewrite (proof_irr Hx Hy); auto.
Qed.

author: lexuanbach

repo: certified-permission-procedure


text:
(*
  Author(s):
    Andrej Dudenhefner (1)
  Affiliation(s):
    (1) Saarland University, Saarbrücken, Germany
*)

(*
  Definition(s):
    Deterministic, Length-preserving Stack Machines
  Problems(s):
    Uniform Boundedness of Deterministic, Length-preserving Stack Machines (SMNdl_UB)
*)

Require Import Relation_Operators List.
Import ListNotations.

Definition State := nat.
Definition Symbol := bool.

Definition Stack : Set := list Symbol.

(* configuration: state, (left stack, right stack) *)
Definition Config : Set := Stack * Stack * State.

(* instruction: vXw -> rYs *)
Definition Instruction : Set := Config * Config.

(* stack machine: list of instructions *)
Definition SMN : Set := list Instruction.

Inductive step (M : SMN) : Config -> Config -> Prop :=
  | transition (v w r s r' s': Stack) (x y: State) :
    In ((r, s, x), (r', s', y)) M ->
    step M (r ++ v, s ++ w, x) (r' ++ v, s' ++ w, y).

(* step is functional *)
Definition deterministic (M: SMN) := forall (X Y Z: Config), step M X Y -> step M X Z -> Y = Z.

(* reflexive transitive closure of step *)
Definition reachable (M: SMN) : Config -> Config -> Prop := clos_refl_trans Config (step M).

(* step is confluent *)
Definition confluent (M: SMN) := forall (X Y1 Y2: Config), reachable M X Y1 -> reachable M X Y2 ->
  exists (Z: Config), reachable M Y1 Z /\ reachable M Y2 Z.

(* uniform bound for the number of reachable configurations *)
Definition bounded (M: SMN) (n: nat) : Prop :=
  forall (X: Config), exists (L: list Config), (forall (Y: Config), reachable M X Y -> In Y L) /\ length L <= n.

(* sum of stack sizes is invariant under step *)
Definition length_preserving (M: SMN) : Prop :=
  forall s t X s' t' Y, In ((s, t, X), (s', t', Y)) M -> length (s ++ t) = length (s' ++ t') /\ 1 <= length (s ++ t).

(* given a deterministic, length-preserving stack machine M,
  is M uniformly bounded by some n? *)
Definition SMNdl_UB : { M : SMN | deterministic M /\ length_preserving M } -> Prop :=
  fun '(exist _ M _) => exists (n: nat), bounded M n.

author: uds-psl

repo: coq-library-undecidability


text:
(******************************************************************************)
(* Dr Daniel Kirk (c) 2021                                                    *)
(******************************************************************************)
(* Let R : ringType and B : eqType                                            *)
(******************************************************************************)
(* hasSupport f s == propositions stating that (s : seq B) contains at        *)
(*                       least the support of (f : B -> R), that is           *)
(*                       forall b : B, ~~(f b == 0) -> b \in s                *)
(*    finSuppE f  == an existential proposition guaranteeing the              *)
(*                       existance of a duplicate-free sequence of B          *)
(*                       containing the support of (f : B -> R), that is      *)
(*                       the support of (f : B -> R), that is                 *)
(*                       exists (s : seq B) (_ : uniq B), hasSupport f s      *)
(*    FSType B    == a record consisting of a function (sort : B -> R),       *)
(*                       and a proof of finSuppE sort                         *)
(*  nullFSType B  == the null function with trivial finite support            *)
(* unitFSType b r == the function with one non-trivial value, that is b |-> r *)
(*                   and b' |-> 0 for all b' != b                             *)
(******************************************************************************)
(* Let s1 s2 : seq B                                                          *)
(******************************************************************************)
(* hasSupport_catl s1 s2 == hasSupport f s1 -> hasSupport f (s1 ++ s2)        *)
(* hasSupport_catl s1 s2 == hasSupport f s2 -> hasSupport f (s1 ++ s2)        *)
(* hasSupport_undup s1   == hasSupport f s1 -> hasSupport f (undup s1)        *)
(******************************************************************************)
(* Let r : R and C D : FSType B                                               *)
(******************************************************************************)
(*   C <+> D    == the FSType that results from adding the underlying         *)
(*                 component-wise                                             *)
(*   r <*:> C   == the FSType that results from adding the underlying         *)
(*                 function component-wise                                    *)
(* C <\oplus> D == the FSType (B + B) that results from constructing the      *)
(*                 disjoint sum of C and D                                    *)
(*  eqFSFun C D == a lemma giving the equivance of C = D as FSTypes and as    *)
(*                 functions. Often used along with functional_extensionality *)
(******************************************************************************)

Require Import Coq.Program.Tactics.
From Coq.Logic Require Import FunctionalExtensionality ProofIrrelevance.
From mathcomp Require Import ssreflect ssrfun eqtype fintype seq bigop.

Require Import Modules Linears.

Set Warnings "-parsing". (* Some weird bug in ssrbool throws out parsing warnings*)
  From mathcomp Require Import ssrbool.
Set Warnings "parsing".

Set Warnings "-ambiguous-paths". (* Some weird bug in ssralg throws out coercion warnings*)
    From mathcomp Require Import ssralg.
Set Warnings "ambiguous-paths".

Open Scope ring_scope.
Set Implicit Arguments.
Unset Strict Implicit.

Import GRing.

Module fsFun.
  Section Def.
    Variable (R : ringType) (B : eqType).

    Definition hasSupport (f : B -> R) (s : seq B) := forall b : B, (f b != 0) -> (b \in s).
    Definition finSuppE (f : B -> R) := exists (s : seq B), uniq s /\ hasSupport f s.
    Record type := Pack {
      sort : B -> R;
      hasFiniteSupport : finSuppE sort;
    }.

    Lemma eqFSFun (C D : type) : C = D <-> (sort C) = (sort D).
    Proof. split; destruct C, D=>/=H. by inversion H.
    by destruct H; rewrite (proof_irrelevance _ hasFiniteSupport0 hasFiniteSupport1).
    Qed.
  End Def.

  Module Exports.
    Notation FSType := type.
    Coercion sort : type >-> Funclass.
  End Exports.

  Section Null.
    Variable (R : ringType) (B : eqType).

    Lemma null_finSuppE : finSuppE (fun _ : B => 0 : R).
    Proof. rewrite/finSuppE.
      refine(ex_intro _ nil _); split=>//.
      by rewrite/hasSupport eq_refl/=.
    Qed.

    Definition null := Pack (null_finSuppE).
  End Null.

  Section Singleton.
    Variable (R : ringType) (B : eqType)
      (b : B) (r : R).

    Lemma unit_finSuppE : finSuppE (fun b' : B => if b' == b then r else 0).
    Proof. rewrite/finSuppE.
      refine(ex_intro _ [::b] _); split=>//.
      rewrite/hasSupport =>b'.
      case (b' == b) as []eqn:E.
      move/eqP in E; destruct E.
      by rewrite in_cons eq_refl orTb.
      by rewrite eq_refl.
    Qed.

    Definition unit := Pack (unit_finSuppE).
  End Singleton.

  Section Results.
    Variable (R : ringType) (B : eqType).
    Import Exports.
    Section FiniteSupports.
      Variable (C : B -> R).
      Lemma hasSupport_catl s1 s2 : hasSupport C s1 -> hasSupport C (s1 ++ s2).
      Proof. rewrite/hasSupport=>H b F.
        by rewrite mem_cat (H b F). Qed.

      Lemma hasSupport_catr s1 s2 : hasSupport C s2 -> hasSupport C (s1 ++ s2).
      Proof. rewrite/hasSupport=>H b F.
        by rewrite mem_cat (H b F) orbT. Qed.

      Lemma hasSupport_undup s : hasSupport C s -> hasSupport C (undup s).
      Proof. rewrite /hasSupport=>H b F.
        by rewrite mem_undup; move: H b F. Qed.

      Lemma hasSupport_perm_eq s1 s2 : (perm_eq s1 s2) -> hasSupport C s1 -> hasSupport C s2.
      Proof. rewrite /hasSupport=>E H b F.
        apply perm_mem in E; rewrite -(E b); apply (H b F).
      Qed.

      Lemma finSupp_cons a s : hasSupport C (a :: s) -> (C a == 0) -> (hasSupport C s).
      Proof. rewrite /hasSupport=>F.
        case (~~(C a == 0)) as []eqn:E=>G.
        by rewrite G in E.
        move=>b V.
        move:(F b V); rewrite in_cons -(rwP orP)=>W.
        destruct W=>//.
        move/eqP in H; destruct H.
        by rewrite G in V.
      Qed.
    End FiniteSupports.
  End Results.

  Section Equality.
    Variable (R : ringType) (B : eqType).
    Import Exports.
    Lemma eqFSSupp (C D : type R B) : C = D <-> exists cd (Ec : hasSupport C cd) (Ed : hasSupport D cd), all (fun b => C b == D b) cd.
    Proof.
      split. destruct C as [c [cs [Uc C]]], D as [d [ds [Ud D]]]=>/=H.
      refine(ex_intro _ (undup(cs ++ ds)) _).
      inversion H; clear H.
      apply (hasSupport_catr cs) in D.
      apply (hasSupport_undup) in D.
      refine(ex_intro _ D _).
      refine(ex_intro _ D _).
      rewrite (eq_all (a2:=predT)).
      apply all_predT.
      by move=>b; rewrite eq_refl.

      move=>H; destruct H as [cd [fsC [fsD A]]].
      rewrite eqFSFun/=.
      apply functional_extensionality=>b.
      move/allP in A.
      case(~~(C b == 0)) as []eqn:Ec.
      move:(fsC _ Ec)=>inC.
      move:(A b inC)=>H.
      by move/eqP in H.
      case(~~(D b == 0)) as []eqn:Ed.
      move:(fsD _ Ed)=>inD.
      move:(A b inD)=>H.
      by move/eqP in H.
      move/negbFE/eqP in Ec.
      move/negbFE/eqP in Ed.
      by rewrite Ec Ed.
    Qed.
  End Equality.

  Section Add.
    Import Exports.
    Variable (R : ringType) (B : eqType) (C D : type R B).
    Lemma addFS : finSuppE (fun b => (C b) + (D b)).
    Proof. destruct C as [c [sc [CU CC]]], D as [d [sd [DU DD]]].
      refine(ex_intro _ (undup(sc ++ sd)) _); split; [apply(undup_uniq _)|].
      move: CC DD.
      rewrite/hasSupport/==> CC DD b H.
      case(~~(c b == 0)) as []eqn:E.
      by rewrite mem_undup mem_cat (CC b E) orTb.
      move/negbFE/eqP in E.
      rewrite E GRing.add0r in H.
      by rewrite mem_undup mem_cat (DD b H) orbT.
    Qed.

    Definition add : type R B := Pack addFS.
  End Add.

  Section Scale.
    Import Exports.
    Variable (R : ringType) (B : eqType) (r : R) (C : type R B).
    Lemma scaleFS : finSuppE (fun b => r * (C b)).
    Proof. destruct C as [c [sc [UC CC]]].
      refine(ex_intro _ sc _); split=>//.
      move: CC.
      rewrite/hasSupport/==> CC b H.
      case(~~(c b == 0)) as []eqn:E.
      by rewrite (CC b E).
      move/negbFE/eqP in E.
      by rewrite E GRing.mulr0 eq_refl in H.
    Qed.

    Definition scale : type R B := Pack scaleFS.
  End Scale.

  Section Sums.
    Import Exports.
      Variable (R : ringType) (B1 B2 : eqType).

      Section Def.
        Variable (C1 : type R B1) (C2 : type R B2).

        Definition sum_fn (b : B1 + B2)
         := match b with inl b' => sort C1 b' | inr b' => sort C2 b' end.

        Definition sum_seq (s1 : seq B1) (s2 : seq B2) := (map inl s1) ++ (map inr s2).

        Lemma sum_uniq s1 s2 (U1 : uniq s1) (U2 : uniq s2) : uniq (sum_seq s1 s2).
        Proof.
          rewrite -(map_inj_in_uniq (f:=@inl B1 B2)) in U1;[|by move=>x y _ _ H; inversion H].
          rewrite -(map_inj_in_uniq (f:=@inr B1 B2)) in U2;[|by move=>x y _ _ H; inversion H].
          rewrite cat_uniq U1 U2 andbT/=-(rwP hasPn)=>x X.
          destruct x.
          by move/mapP in X; destruct X.
          rewrite -(rwP negP)=>Y.
          by move/mapP in Y; destruct Y.
        Qed.

        Lemma sumFS : finSuppE sum_fn.
        Proof. rewrite/sum_fn.
          destruct C1 as [c1 [s1 [U1 S1]]], C2 as [c2 [s2 [U2 S2]]].
          refine(ex_intro _ (sum_seq s1 s2) _); split; [apply (sum_uniq U1 U2)|].
          move=>b C; destruct b.
          move:(S1 s C)=>D.
          apply (map_f (@inl B1 B2)) in D.
          by rewrite mem_cat D.
          move:(S2 s C)=>D.
          apply (map_f (@inr B1 B2)) in D.
          by rewrite mem_cat D orbT.
        Qed.

        Definition sum : type R (sum_eqType B1 B2) := Pack sumFS.
      End Def.

      Section Def.
        Variable (C : type R (sum_eqType B1 B2)).

        Definition foldL (c : seq (sum_eqType B1 B2)) : seq  B1
          := foldr (fun br (L : seq B1) => if br is inl br'
            then br'::L else L) nil c.
        Lemma foldL_consl a (c : seq (sum_eqType B1 B2))
            : foldL ((inl a)::c) = a :: foldL c.
        Proof. by []. Qed.
        Lemma foldL_consr a (c : seq (sum_eqType B1 B2))
            : foldL ((inr a)::c) = foldL c.
        Proof. by []. Qed.

        Lemma subseql (c : seq (sum_eqType B1 B2)) :
          subseq (map (@inl B1 B2) (foldL c)) c.
        Proof. induction c=>//.
          destruct a; [rewrite foldL_consl| rewrite foldL_consr].
          by rewrite /=eq_refl IHc.
          apply (subseq_trans IHc (subseq_cons _ _)).
        Qed.

        Lemma foldL_uniq s : uniq s -> uniq (foldL s).
        Proof. move=>U.
          apply (subseq_uniq (subseql s)) in U.
          rewrite -(map_inj_in_uniq (f:=@inl B1 B2))=>//.
          move=>x y _ _ H; by inversion H.
        Qed.

        Lemma foldL_fs (c : sum_eqType B1 B2 -> R) s : hasSupport c s -> hasSupport (c \o inl) (foldL s).
        Proof. rewrite/comp=>S b B.
          move: (S (inl b) B); clear S.
          induction s=>//.
          rewrite in_cons -(rwP orP)=>X.
          destruct X.
          move/eqP in H.
          by rewrite -H foldL_consl in_cons eq_refl.
          destruct a.
          by rewrite foldL_consl in_cons (IHs H) orbT.
          by rewrite foldL_consr (IHs H).
        Qed.

        Lemma lsumFS : finSuppE (C \o inl).
        Proof. destruct C as [c [s [U S]]].
          refine(ex_intro _ (foldL s) _); split; [apply(foldL_uniq U)|apply(foldL_fs S)].
        Qed.

        Definition foldFSl := Pack lsumFS.

        Definition foldR (c : seq (sum_eqType B1 B2)) : seq  B2
          := foldr (fun br (L : seq B2) =>
        if br is inr br' then br'::L else L
          ) nil c.
        Lemma foldR_consr a (c : seq (sum_eqType B1 B2))
            : foldR ((inr a)::c) = a :: foldR c.
        Proof. by []. Qed.
        Lemma foldR_consl a (c : seq (sum_eqType B1 B2))
            : foldR ((inl a)::c) = foldR c.
        Proof. by []. Qed.

        Lemma subseqr (c : seq (sum_eqType B1 B2)) :
          subseq (map (@inr B1 B2) (foldR c)) c.
        Proof. induction c=>//.
          destruct a; [rewrite foldR_consl| rewrite foldR_consr].
          apply (subseq_trans IHc (subseq_cons _ _)).
          by rewrite /=eq_refl IHc.
        Qed.

        Lemma foldR_uniq s : uniq s -> uniq (foldR s).
        Proof. move=>U.
          apply (subseq_uniq (subseqr s)) in U.
          rewrite -(map_inj_in_uniq (f:=@inr B1 B2))=>//.
          move=>x y _ _ H; by inversion H.
        Qed.

        Lemma foldR_fs (c : sum_eqType B1 B2 -> R) s : hasSupport c s -> hasSupport (c \o inr) (foldR s).
        Proof. rewrite/comp=>S b B.
          move: (S (inr b) B); clear S.
          induction s=>//.
          rewrite in_cons -(rwP orP)=>X.
          destruct X.
          move/eqP in H.
          by rewrite -H foldR_consr in_cons eq_refl.
          destruct a.
          by rewrite foldR_consl (IHs H).
          by rewrite foldR_consr in_cons (IHs H) orbT.
        Qed.

        Lemma rsumFS : finSuppE (C \o inr).
        Proof. destruct C as [c [s [U S]]].
          refine(ex_intro _ (foldR s) _); split; [apply(foldR_uniq U)|apply(foldR_fs S)].
        Qed.

        Definition foldFSr := Pack rsumFS.
      End Def.
      Section Result.
        Variable (C1 : type R B1) (C2 : type R B2).

        Lemma hasFunSupp_sum s1 s2 : hasSupport C1 s1 -> hasSupport C2 s2
          -> hasSupport (sum C1 C2) (sum_seq s1 s2).
          Proof.
            move=>H1 H2 b C.
            rewrite mem_cat.
            destruct b.
            simpl in C.
            move: (H1 _ C)=>D1.
            apply (map_f (@inl B1 B2)) in D1.
            by rewrite D1.
            simpl in C.
            move: (H2 _ C)=>D2.
            apply (map_f (@inr B1 B2)) in D2.
            by rewrite D2 orbT.
          Qed.
    End Result.
  End Sums.

End fsFun.
Export fsFun.Exports.
Notation hasSupport := fsFun.hasSupport.
Notation finSuppE := fsFun.finSuppE.
Notation nullFSType := fsFun.null.
Notation unitFSType := fsFun.unit.
Notation eqFSFun := fsFun.eqFSFun.
Infix "<+>" := fsFun.add (at level 39) : lmod_scope.
Infix "<*:>" := fsFun.scale (at level 39) : lmod_scope.
Infix "<\oplus>" := (fsFun.sum) (at level 39) : lmod_scope.

author: Modularius

repo: MathcompFreeModules


text:
Require Export Setoid Coq.Classes.Morphisms Omega.
Require Export Sets SetInterface SetConstructs SetProperties.
Require Import EqDec CSetNotation CSetTac CSetComputable.
Require Import CSetDisjoint CSetGet Drop AllInRel.

Set Implicit Arguments.

Definition pairwise_ne {X} (P:X->X->Prop) (L:list X) :=
  forall n m a b, n <> m -> get L n a -> get L m b -> P a b.

Lemma pairwise_ne_rev X (P:relation X) (L: list X)
: pairwise_ne P L
  -> pairwise_ne P (rev L).
Proof.
  intros; hnf; intros.
  exploit (get_range H1); eauto.
  exploit (get_range H2); eauto.
  eapply get_rev in H1.
  eapply get_rev in H2.
  eapply H; try eapply H1; try eapply H2; eauto.
  rewrite rev_length in H3.
  rewrite rev_length in H4.
  omega.
Qed.

Definition pairwise_disj_PIR2 X `{OrderedType X} L L'
: pairwise_ne disj L
  -> PIR2 Equal L L'
  -> pairwise_ne disj L'.
Proof.
  unfold pairwise_ne; intros.
  eapply PIR2_nth_2 in H3; eauto; dcr.
  eapply PIR2_nth_2 in H4; eauto; dcr.
  rewrite <- H7, <- H8; eauto.
Qed.

Fixpoint pw_disj X `{OrderedType X} (L:list (set X)) :=
  match L with
    | x::xs => disj x (list_union xs) /\ pw_disj xs
    | nil => True
  end.

Lemma pw_disj_get X `{OrderedType X} (L:list (set X)) n s
: pw_disj L -> get L n s -> disj s (list_union (drop (S n) L)).
Proof.
  intros. general induction H1; simpl in * |- *; eauto.
Qed.

Lemma pw_disj_pairwise_disj X `{OrderedType X} (L:list (set X))
: pw_disj L -> pairwise_ne disj L.
Proof.
  intros. hnf; intros.
  exploit pw_disj_get; try eapply H2; eauto.
  exploit pw_disj_get; try eapply H3; eauto.
  decide (n < m).
  - eapply disj_2_incl; eauto. eapply incl_list_union.
    eapply drop_get. instantiate (2:=m - S n).
    orewrite (S n + (m - S n) = m); eauto. eauto.
  - symmetry. eapply disj_2_incl; eauto.
    eapply incl_list_union.
    eapply drop_get. instantiate (2:=n - S m).
    orewrite (S m + (n - S m) = n); eauto. eauto.
Qed.

Definition disjoint X `{OrderedType X} (DL:list (option (set X))) (G:set X) :=
  forall n s, get DL n (Some s) -> disj s G.

Lemma disjoint_incl X `{OrderedType X} L D D'
  : disjoint L D
    -> D' ⊆ D
    -> disjoint L D'.
Proof.
  firstorder.
Qed.

Instance disjoint_morphism_subset X `{OrderedType X}
  : Proper (eq ==> Subset ==> flip impl) (@disjoint X _).
Proof.
  unfold Proper, respectful, impl, flip, disj, disjoint; intros; subst.
  rewrite H1; eauto.
Qed.

Instance disjoint_morphism X `{OrderedType X}
  : Proper (eq ==> Equal ==> iff) (@disjoint X _).
Proof.
  unfold Proper, respectful, iff, disjoint; split; intros; subst.
  - rewrite <- H1; eauto.
  - rewrite H1; eauto.
Qed.

Lemma disjoint_app X `{OrderedType X} L L' (D:set X)
: disjoint (L ++ L') D <-> disjoint L D /\ disjoint L' D.
Proof.
  split; unfold disjoint.
  - split; intros; eauto using get_shift, get_app.
  -intros. eapply get_app_cases in H1; intuition; eauto.
Qed.

author: sigurdschneider

repo: lvc

save_path: github-repos/coq/sigurdschneider-lvc


text:
Require Import FiniteOrderMeasure.
Require Import Coq.Arith.Compare_dec.
Require Import Lia.
Require Import PeanoNat.
Import Nat Lt Le.
Require Import List.
Import ListNotations.

Module Type TypeMod.
Parameter A : Type.
End TypeMod.

(* needs to be outside the FtreeMod module because of a limitation of the Coq module system *)

Inductive Ftree{A:Type} : Type   :=
|bot : Ftree
|ftree : A-> list Ftree -> Ftree.

Module FtreeMod (TM : TypeMod) <: FiniteOrderMeasureMod.
Import TM.

Lemma Ftree_induct : forall (P : Ftree (A:=A)-> Prop),
    P bot ->
    (forall a l,
            (forall n, n < length l ->  P (nth n l bot))
            -> P (ftree a l))  ->
    forall t,  P t.
Proof.
intros P Hn Hall.
fix Ftree_induct_t 1.
intro t.
destruct t.
*
 apply Hn.
*
  apply Hall.
  induction l; intros n Hlt;  cbn in Hlt ; [lia|].
  destruct n; cbn.
  +
    apply  Ftree_induct_t.
  +
    apply IHl ; lia.
Qed.

Fixpoint cut (n : nat) (t : Ftree(A:=A)) : Ftree(A:=A) :=
match n with
| 0 => bot
|S m =>
 match t with
 |bot => bot
 |ftree a l => ftree a (map (cut m) l)
 end
end.

Fixpoint height (t : Ftree(A:=A)) : nat :=
match t with
bot => 0
| ftree a l => S (list_max (map height l))
end.

Lemma cut_above_height : forall  t n, height t <= n -> cut n t = t.
Proof.
induction t0 using Ftree_induct; intros n Hle ; auto.
*
  destruct n ; auto.
*
  revert l H n Hle.
  induction l; intros H n Hle; auto; cbn.
  +
    destruct n ;  cbn in Hle ; try lia; auto.
  +
    destruct n ;  cbn in Hle ; try lia.
    apply le_S_n in Hle.
    cbn.
    f_equal.
    f_equal.
    -
      generalize (H _ (Nat.lt_0_succ _)); intro Ha0.
      cbn [nth] in Ha0.
      apply Ha0.
      apply le_trans with (m := max (height a0)
          (fold_right Init.Nat.max
                      0 (map height l))); auto.
      apply Max.le_max_l.
   -
      assert (Hl :  forall n : nat,
        height (ftree a l) <= n ->
        cut n (ftree a l) =
        ftree a l).
      {
        eapply IHl ; eauto.
        intros j Hlt i Hh.
        specialize (H (S j)).
        apply H; auto.
        cbn ; lia.
      }
      specialize (Hl (S n)).
      cbn in Hl.
      assert (Heqtree :  ftree a (map (cut n) l) = ftree a l).
      {
        apply Hl,  le_n_S .
        apply le_trans with (m := max (height a0)
          (fold_right max 0
                      (map height l))); auto.
        apply Max.le_max_r.
      }
     injection Heqtree; intros; auto.
Qed.

Lemma max_list_max :
  forall l n, n < length l -> height (nth n l bot) <=   list_max (map height l).
Proof.
induction l; intros n Hlt; cbn in Hlt ; try lia.
destruct n; cbn; try lia.
replace ((fold_right Init.Nat.max 0
                     (map height l))) with (list_max (map height l)); auto.

apply lt_S_n in Hlt.
specialize (IHl _  Hlt).
eapply le_trans ; eauto.
apply Max.le_max_r.
Qed.

Lemma map_cut : forall l n,
    list_max (map height l) <= n -> map (cut n) l = l.
Proof.
induction l; intros n Hle; auto.
cbn.
f_equal.
{
  rewrite cut_above_height; auto.
  apply le_trans  with (m := list_max
                               (map height (a :: l))); eauto.
 apply Max.le_max_l.
}
{
  eapply IHl; eauto.
  apply le_trans with (m := list_max
                              (map height (a :: l))); eauto.
  apply Max.le_max_r.
}
Qed.

Lemma cut_reaches_max :
  forall l, (forall n : nat,
      n < length l ->
      forall k : nat,
      (k < height (nth n l bot) ->
       height (cut k (nth n l bot)) = k)) ->
            forall n,  n < list_max (map height l) ->
                       list_max (map height (map (cut n) l)) = n.
Proof.
induction l; intros Hall n Hlt; cbn in Hlt; try lia.
cbn [map].
unfold list_max.
cbn.
replace ( (fold_right Init.Nat.max 0
                      (map height (map (cut n) l)))) with
    (list_max (map height (map (cut n) l))) ; auto.
replace ((fold_right Init.Nat.max 0
                     (map height l))) with (
                                          list_max (map height l)) in Hlt; auto.
specialize (Hall _ (Nat.lt_0_succ _) n) as Ha.
cbn in Ha.
 case (le_lt_dec (height a) ((list_max (map height l)))  ); intro Hcas.
{
   assert (Hrn : n <  list_max (map height l)); [lia|].
  remember   (list_max (map height (map (cut n) l)))  as max_rest.
  assert (Hmr : max_rest = n).
  {
    subst.
    eapply IHl; eauto.
    intros.
    specialize (Hall (S n0)); cbn in Hall.
    apply Hall; auto.
    cbn; lia.
  }
  rewrite Hmr.
  apply Nat.max_r.
  case (le_lt_dec (height a) n); intro Hcas'.
  *
    now rewrite cut_above_height.
  *
    now rewrite Ha.
}
{
  assert (Hrn : n <  height a); [lia|].
  rewrite Ha; auto.
  remember   (list_max (map height (map (cut n) l)))  as max_rest.
  apply Nat.max_l.
  case(le_lt_dec (list_max (map height l)) n); intro Hcas''.
  2 :
    {
    assert (Hmr : max_rest = n).
    {
      subst.
      eapply IHl; eauto.
      intros.
      specialize (Hall (S n0)); cbn in Hall.
      apply Hall; auto.
      cbn ; lia.
    }
    rewrite Hmr; auto.
  }
  subst.
  rewrite map_cut; auto.
}
Qed.

Lemma cut_below_height : forall  t n,
   n <= height t -> height (cut n t) = n.
Proof.
intros t n Hle.
destruct (le_lt_eq_dec _ _ Hle).
*
  clear Hle; revert n l.
  induction t using Ftree_induct;  intro n.
  +
    intro Hlt;  cbn in Hlt ; destruct n; try lia; auto.
  +
    intro Hlt.
    destruct n; auto.
    cbn in Hlt.
    cbn.
    f_equal.
    apply lt_S_n in Hlt.
    now apply cut_reaches_max.
*
  rewrite cut_above_height; auto; lia.
Qed.

Lemma cut_n_Sn : forall n t, n < height t -> cut n t = cut n (cut (S n) t).
Proof.
induction n as [ | n IHn]; [reflexivity | ].
intros [ | a l] Hlt; cbn in Hlt; [lia | ].
cbn.
f_equal.
revert n IHn Hlt.
induction l as [ | t l IHl]; intros n IHn Hlt; [reflexivity | ].
cbn [map] in Hlt.
change (height t :: map height l) with ([height t] ++ map height l) in Hlt.
rewrite list_max_app in Hlt.
cbn.
f_equal.
- apply lt_S_n, Nat.max_le in Hlt.
  destruct Hlt as [Hlt | Hlt].
  + cbn in Hlt.
    rewrite Nat.max_0_r in Hlt.
    apply IHn.
    lia.
  + change (match t with
  | bot => bot
  | ftree a l0 => ftree a (map (cut n) l0)
  end) with (cut (S n) t).
  destruct (le_lt_dec (height t) n) as [Hle | Hlt'].
  * f_equal.
    rewrite cut_above_height; [reflexivity | lia].
  * apply IHn, Hlt'.
- apply lt_S_n in Hlt.
  destruct (le_lt_dec (list_max (map height l)) (list_max [height t]))
   as [Hle | Hlt'].
  + cbn in Hlt, Hle.
    rewrite Nat.max_0_r in Hlt, Hle.
    change (fun t0 : Ftree =>
      match t0 with
      | bot => bot
      | ftree a0 l0 => ftree a0 (map (cut n) l0)
      end) with (cut (S n)).
    (* Search (_ <= _ -> max _ _ = _). *)
    rewrite max_l in Hlt by apply Hle.
    clear a IHl.
    induction l as [ | t' l IH]; [reflexivity | ].
    cbn [map].
    f_equal.
    * destruct (le_lt_dec (height t') (S n)) as [Hle' | Hlt'].
      -- f_equal.
         rewrite cut_above_height; [reflexivity | exact Hle'].
      -- apply IHn.
         lia.
    * apply IH.
      cbn [map] in Hle.
      change (height t' :: map height l) with ([height t'] ++ map height l) in Hle.
      rewrite list_max_app in Hle.
      lia.
  + apply IHl; [exact IHn | lia].
Qed.

Definition fprefix (t1 t2: Ftree) :Prop := t1 = cut (height t1) t2.

Lemma fprefix_refl : forall t,  fprefix t t.
Proof.
intro t.
unfold fprefix.
rewrite cut_above_height; auto.
Qed.

Lemma fprefix_height : forall t1 t2,  fprefix t1 t2 -> height t1 <= height t2.
Proof.
unfold fprefix ; intros t1 t2 Hpre.
case (le_lt_dec (height t1) (height t2)); intros Hcas; auto.
exfalso.
rewrite cut_above_height in Hpre; try lia.
rewrite Hpre in Hcas; lia.
Qed.

Definition cut_last (t : Ftree) : Ftree := cut (pred (height t)) t.

Lemma cut_last_S  : forall n t, n < height t -> cut n t = cut_last (cut (S n) t).
Proof.
intros n t Hle.
unfold cut_last.
rewrite cut_below_height; auto.
rewrite Nat.pred_succ; try lia.
rewrite cut_n_Sn; auto.
Qed.

Lemma cut_twice : forall n m t, n <= m ->
cut n (cut m t) = cut n t.
intros n m t Hle.
revert t.
induction Hle; intro t.
*
  case (le_lt_dec n (height t)); intros Hcas.
  +
    assert (Hc : height (cut n t) = n); [apply cut_below_height; auto |].
    apply cut_above_height; lia.
  +
    assert (Heq: cut n t = t).
    {
      rewrite cut_above_height; auto ; lia.
    }
    repeat rewrite Heq ; auto.
*
  destruct t; auto.
  cbn.
  destruct n; auto.
  cbn.
  f_equal.
  revert n m Hle IHHle a.
  induction l; intros n m Hle IHHle a'; auto.
  cbn.
  f_equal.
  +
    specialize (IHHle a).
    case (le_lt_dec (height a) m); intros Hcas.
    {
      rewrite (cut_above_height _ m); auto.
    }
    rewrite cut_last_S; auto.
    {
      rewrite IHHle.
      replace (cut n a) with (cut_last (cut (S n) a)); [rewrite <- IHHle; auto |].
      symmetry.
      apply  cut_last_S; lia.
    }
    {
      rewrite cut_below_height; auto; lia.
    }
  +
    rewrite IHl; auto.
Qed.

Lemma fprefix_trans : forall t1 t2 t3, fprefix t1 t2 -> fprefix t2 t3 -> fprefix t1 t3.
Proof.
unfold fprefix; intros t1 t2 t3 Hpre1 Hpre2.
remember (height t1) as h1.
rewrite Hpre1; subst.
rewrite Hpre2.
apply fprefix_height in Hpre1, Hpre2.
apply cut_twice; auto.
Qed.

Lemma fprefix_antisym :
  forall t1 t2,  fprefix t1 t2 -> fprefix t2 t1 -> t1 = t2.
Proof.
intros t1 t2 Hpre1 Hpre2.
unfold fprefix in *.
case (le_lt_dec (height t1) (height t2)); intros Hcas.
*
  rewrite cut_above_height in Hpre2; auto.
*
  rewrite cut_above_height in Hpre1; auto; lia.
Qed.

Lemma fprefix_wtotal_l :
  forall t t1 t2,
    fprefix t1 t -> fprefix t2 t ->
    height t1  <= height t2 ->
    fprefix t1 t2.
Proof.
intros t t1 t2 Hpre1 Hpre2 Hle.
unfold fprefix in *.
rewrite Hpre2.
rewrite cut_twice; auto.
Qed.

Lemma fprefix_wtotal_r :
  forall t t1 t2,
    fprefix t1 t -> fprefix t2 t ->
    height t2  <= height t1 ->
    fprefix t2 t1.
Proof.
intros t t1 t2 Hpre1 Hpre2 Hle.
unfold fprefix in *.
rewrite Hpre1.
rewrite cut_twice; auto.
Qed.

Lemma fprefix_wtotal : forall t1 t2 t,
    fprefix t1 t -> fprefix t2 t -> (fprefix t1 t2 \/ fprefix t2 t1).
Proof.
intros t1 t2 t Hp1 Hp2.
destruct (le_gt_dec (height t1) (height t2)).
*
  left.
  eapply fprefix_wtotal_l; eauto.
*
  right.
  eapply fprefix_wtotal_r; eauto; lia.
Qed.

Lemma fprefix_height_eq_or_lt :
  forall t1 t2, fprefix t1 t2 -> t1 = t2 \/ height t1 < height t2.
Proof.
induction t1 using Ftree_induct.
*
  intros t2 Hpre.
  destruct t2; [left ; auto| right; cbn; lia].
*
  intros t2 Hpre.
  destruct t2.
  +
    exfalso.
    unfold fprefix in Hpre.
    discriminate.
  +
    unfold fprefix in Hpre.
    destruct (le_gt_dec (height (ftree a0 l0)) (height (ftree a l))).
    -
      rewrite cut_above_height in Hpre; auto.
    -
      right; lia.
Qed.

Definition Cc : Type := Ftree(A:=A).

Definition bot := bot (A:=A).

Definition ordc := fprefix.

Definition sordc x y := ordc x y /\ x <> y.

Lemma bot_is_bot : forall x, ordc bot x.
Proof.
intro x; constructor.
Qed.

Definition ordc_refl := fprefix_refl.

Definition ordc_trans := fprefix_trans.

Definition ordc_antisym := fprefix_antisym.

Definition  ordc_wtotal := fprefix_wtotal.

Definition mu := height.

Lemma mu_sordc : forall x y, ordc x y -> x <> y ->  mu x < mu y.
Proof.
intros x y Ho Hne.
apply fprefix_height_eq_or_lt in Ho.
destruct Ho as [Ho |Ho]; auto.
exfalso; now apply Hne.
Qed.

End FtreeMod.

author: hidden-author


text:
(* ******************************************************************************* *)
(** * Yoneda embedding
    Niccolò Veltri, Niels van der Weide
    April 2019
 ********************************************************************************* *)

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.PseudoFunctors.Display.Base.
Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells.
Require Import UniMath.Bicategories.PseudoFunctors.Display.Map2Cells.
Require Import UniMath.Bicategories.PseudoFunctors.Display.Identitor.
Require Import UniMath.Bicategories.PseudoFunctors.Display.Compositor.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.Bicategories.Core.Examples.OpMorBicat.
Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.PseudoFunctors.Representable.
Require Import UniMath.Bicategories.Transformations.PseudoTransformation.
Require Import UniMath.Bicategories.Modifications.Modification.

Local Open Scope bicategory_scope.
Local Open Scope cat.

Section Yoneda.

Context {C : bicat}.
Variable (C_is_univalent_2_1 : is_univalent_2_1 C).

Definition representable_id_inv2cell (X : C)
  : invertible_modification_data (id_pstrans (representable C_is_univalent_2_1 X))
                                 (representable1 C_is_univalent_2_1 (id₁ X)).
Proof.
  intro Y.
  use make_invertible_2cell.
  - use make_nat_trans.
    * intro f.
      cbn in *.
      apply rinvunitor.
    * abstract
        (intros f g η ;
         cbn in * ;
         rewrite rwhisker_hcomp ;
         apply rinvunitor_natural).
  - use make_is_invertible_2cell.
    + use make_nat_trans.
      * intro f.
        cbn in *.
        apply runitor.
      * abstract (intros f g η ; cbn ; apply vcomp_runitor).
    + use nat_trans_eq.
      { exact (pr2 C Y X). }
      abstract (intro f ;
                cbn in * ;
                apply rinvunitor_runitor).
    + use nat_trans_eq.
      { exact (pr2 C Y X). }
      abstract (intro f ;
                cbn in * ;
                apply runitor_rinvunitor).
Defined.

Definition representable_id_is_mod (X : C)
  : is_modification (representable_id_inv2cell X).
Proof.
  intros Y Z f.
  use nat_trans_eq.
  { exact (pr2 C Z X). }
  intro g.
  cbn in *.
  repeat (rewrite id2_left).
  symmetry.
  apply rinvunitor_triangle.
Qed.

Definition representable_id_invmod (X : C)
  : invertible_modification (id_pstrans _) (representable1 C_is_univalent_2_1 (id₁ X)).
Proof.
  use make_invertible_modification.
  - exact (representable_id_inv2cell X).
  - exact (representable_id_is_mod X).
Defined.

Definition representable_comp_inv2cell {X Y Z: C} (f : X --> Y) (g : Y --> Z)
  : invertible_modification_data
      (comp_pstrans (representable1 C_is_univalent_2_1 f)
                  (representable1 C_is_univalent_2_1 g))
      (representable1 C_is_univalent_2_1 (f · g)).
Proof.
  intro W.
  use make_invertible_2cell.
  - use make_nat_trans.
    + intro h.
      cbn in *.
      apply rassociator.
    + abstract (intros V U h;
                cbn in *;
                apply rwhisker_rwhisker_alt).
  - use make_is_invertible_2cell.
    + use make_nat_trans.
      * intro h.
        cbn in *.
        apply lassociator.
      * abstract (intros h k η;
                  cbn in *;
                  symmetry;
                  apply rwhisker_rwhisker).
    + use nat_trans_eq.
      { exact (pr2 C W Z). }
      abstract (intro h;
                cbn in *;
                apply rassociator_lassociator).
    + use nat_trans_eq.
      { exact (pr2 C W Z). }
      abstract (intro h;
                cbn in *;
                apply lassociator_rassociator).
Defined.

Definition representable_comp_is_mod {X Y Z: C} (f : X --> Y) (g : Y --> Z)
  : is_modification (representable_comp_inv2cell f g).
Proof.
  intros W V h.
  use nat_trans_eq.
  { exact (pr2 C V Z). }
  intros k.
  cbn in *.
  repeat (rewrite id2_left).
  repeat (rewrite id2_right).
  rewrite rwhisker_hcomp.
  rewrite <- vassocr.
  symmetry.
  rewrite lwhisker_hcomp.
  apply inverse_pentagon_5.
Qed.

Definition representable_comp_invmod {X Y Z: C} (f : X --> Y) (g : Y --> Z)
  : invertible_modification
      (comp_pstrans (representable1 C_is_univalent_2_1 f)
                  (representable1 C_is_univalent_2_1 g))
      (representable1 C_is_univalent_2_1 (f · g)).
Proof.
  use make_invertible_modification.
  - exact (representable_comp_inv2cell f g).
  - exact (representable_comp_is_mod f g).
Defined.

Definition y_data : psfunctor_data C (psfunctor_bicat (op1_bicat C) bicat_of_univ_cats).
Proof.
  use make_psfunctor_data.
  - exact (representable C_is_univalent_2_1).
  - intros X Y.
    exact (representable1 C_is_univalent_2_1).
  - intros X Y f g.
    exact (representable2 C_is_univalent_2_1).
  - intro X.
    apply (representable_id_invmod X).
  - intros X Y Z f g.
    apply (representable_comp_invmod f g).
Defined.

Definition y_laws : psfunctor_laws y_data.
Proof.
  repeat split; cbn.
  - intros X Y f.
    use modification_eq.
    intro Z.
    use nat_trans_eq.
    { exact (pr2 C Z Y). }
    intro g.
    cbn in *.
    apply lwhisker_id2.
  - intros X Y f g h η φ.
    use modification_eq.
    intro Z.
    use nat_trans_eq.
    { exact (pr2 C Z Y). }
    intro k.
    cbn in *.
    symmetry.
    apply lwhisker_vcomp.
  - intros X Y f.
    use modification_eq.
    intro Z.
    use nat_trans_eq.
    { exact (pr2 C Z Y). }
    intro g.
    cbn in *.
    symmetry.
    rewrite <- vassocr.
    rewrite lunitor_lwhisker.
    rewrite rwhisker_vcomp.
    rewrite rinvunitor_runitor.
    apply id2_rwhisker.
  - intros X Y f.
    use modification_eq.
    intro Z.
    use nat_trans_eq.
    { exact (pr2 C Z Y). }
    intro g.
    cbn in *.
    symmetry.
    rewrite <- vassocr.
     rewrite runitor_triangle.
    apply rinvunitor_runitor.
  - intros X Y Z W f g h.
    use modification_eq.
    intro V.
    use nat_trans_eq.
    { exact (pr2 C V W). }
    intro k.
    cbn in *.
    rewrite id2_left.
    symmetry.
    rewrite rwhisker_hcomp.
    rewrite inverse_pentagon_6.
    rewrite lwhisker_hcomp.
    apply vassocr.
  - intros X Y Z f g h η.
    use modification_eq.
    intro W.
    use nat_trans_eq.
    { exact (pr2 C W Z). }
    intro k.
    cbn in *.
    apply lwhisker_lwhisker_rassociator.
  - intros X Y Z f g h η.
    use modification_eq.
    intro W.
    use nat_trans_eq.
    { exact (pr2 C W Z). }
    intro k.
    cbn in *.
    apply rwhisker_lwhisker_rassociator.
Qed.

Definition y_invertible_cells : invertible_cells y_data.
Proof.
  split.
  - intro X.
    apply (representable_id_invmod X).
  - intros X Y Z f g.
    apply (representable_comp_invmod f g).
Defined.

Definition y : psfunctor C (psfunctor_bicat (op1_bicat C) bicat_of_univ_cats).
Proof.
  use make_psfunctor.
  - exact y_data.
  - exact y_laws.
  - exact y_invertible_cells.
Defined.

End Yoneda.

author: UniMath

repo: UniMath

save_path: github-repos/coq/UniMath-UniMath


text:
Load LFindLoad.
From lfind Require Import LFind.
From QuickChick Require Import QuickChick.
From adtind Require Import goal4.

Derive Show for natural.

              Derive Arbitrary for natural.

              Instance Dec_Eq_natural : Dec_Eq natural.

              Proof. dec_eq. Qed.
Derive Show for lst.

              Derive Arbitrary for lst.

              Instance Dec_Eq_lst : Dec_Eq lst.

              Proof. dec_eq. Qed.

Lemma conj11eqsynthconj5 : forall  (lv0 : lst) (lv1 : lst), (@eq lst (append lv0 lv1) (append Nil (append lv0 lv1))).
Admitted.
QuickChick conj11eqsynthconj5.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker