text:
Set Implicit Arguments.

Create HintDb mono discriminated.

Section ExPath.

Variable cfg : Set.
Variable step : cfg -> cfg -> Prop.

(* The actual semantic notion of reachability *)
CoInductive reaches (x : cfg) (P : cfg -> Prop) : Prop :=
  | Done : P x -> reaches x P
  | Step : (exists y, step x y) ->
           (forall y, step x y -> reaches y P) -> reaches x P
  .

Definition RRel : Type := cfg -> (cfg -> Prop) -> Prop.
Definition subrel (A B : RRel) : Prop := forall x P, A x P -> B x P.
Lemma subrel_trans (A B C : RRel) : subrel A B -> subrel B C -> subrel A C.
Proof. firstorder. Qed.

(* A set of claimed proerties is sound if all are valid *)
Definition sound (X : RRel) : Prop := subrel X reaches.

(* To prove soundness, we will use coinduction *)
(* First, here is a functor of which reaches is the greatest fixpoint *)
Inductive stepF (X : RRel) (x : cfg) (P : cfg -> Prop) : Prop :=
  | DoneF : P x -> stepF X x P
  | StepF : (exists y, step x y) ->
            (forall y, step x y -> X y P) -> stepF X x P.
(* To show it's actually a functor, we need to prove monotonicity. *)

Definition mono (F : RRel -> RRel) := forall A B, subrel A B -> subrel (F A) (F B).
Lemma step_mono : mono stepF.
(* For most simple types, we just need to do a case analysis, apply the
   hypothesis if applicable, and reapply some constructor, so name the tactic*)
Ltac mono_tac typename := induction 2;eauto using typename.
mono_tac stepF.
Qed.
Hint Resolve step_mono : mono.

(* Now that we have a functor, we'll show reaches is a fixpoint *)
Lemma reaches_fixed : forall x P, reaches x P <-> stepF reaches x P.
split;destruct 1;eauto using stepF,reaches.
Qed.

(* One equivalent definition of being the greatest fixpoint of
   F is that a fixpoint includes every F-stable set *)

(* A set of claims is stable if each is also justified by
   stepF from other claims in the set *)
Definition stable (X : RRel) : Prop := subrel X (stepF X).

CoFixpoint stable_sound X (Hstable : stable X) : sound X.
intros x P HxP.
apply Hstable in HxP. destruct HxP.
apply Done;assumption.
apply Step. assumption.
   intros y Hstep.
    unfold sound,subrel in stable_sound.
    apply (stable_sound _ Hstable).
    clear stable_sound. auto.
Qed.

Inductive trans (X : RRel) (x : cfg) (P : cfg -> Prop) : Prop :=
| Trans : forall Q, X x Q -> (forall t, Q t -> X t P) -> trans X x P.

Lemma trans_mono : mono trans.
firstorder.
Qed.

Inductive derivedF (F : RRel -> RRel)
                   (X : RRel) (x : cfg) (P : cfg -> Prop) : Prop :=
  | dleaf : X x P -> derivedF F X x P
  | dstep : stepF (derivedF F X) x P -> derivedF F X x P
  | drule' : forall (Q : RRel), subrel Q (derivedF F X) ->
                                F Q x P -> derivedF F X x P.
Definition drule F X x P : F (derivedF F X) x P -> derivedF F X x P :=
  drule' _ _ (fun _ _ H => H).

Definition union (F G : RRel -> RRel) : RRel -> RRel :=
  fun X x P => F X x P \/ G X x P.
Lemma union_mono F G : mono F -> mono G -> mono (union F G).
firstorder.
Qed.

Definition comp_valid (F : RRel -> RRel) : Prop :=
  forall X, subrel (F (stepF X)) (stepF (derivedF F X)).

(* This makes it clear it doesn't matter what other rules
   are used, X could be of the form derivedF (F + G') B,
   and by unioning it reduces to this
 *)

Lemma trans_valid : comp_valid trans.
unfold comp_valid.
destruct 1.
destruct H.
specialize (H0 _ H).
revert H0. apply step_mono. unfold subrel; auto using dleaf.
apply StepF.
assumption.
intros y Hstep.
specialize (H1 y Hstep).
apply drule.
eapply Trans.
apply dleaf.
eassumption.
intros t Qt.
specialize (H0 t Qt).
clear -H0.
apply dstep.
revert H0.
apply step_mono.
clear.
unfold subrel;auto using dleaf.
Qed.

End ExPath.

author: Formal-Systems-Laboratory

repo: coinduction


text:
Require Import Coq.FSets.FMapPositive Coq.PArith.BinPos Coq.Lists.List.

Set Asymmetric Patterns.

Notation eta x := (fst x, snd x).

Inductive expr {var : Type} : Type :=
| Const : expr
| LetIn : expr -> (var -> expr) -> expr.

Definition Expr := forall var, @expr var.

Fixpoint count_binders (e : @expr unit) : nat :=
match e with
| LetIn _ eC => 1 + @count_binders (eC tt)
| _ => 0
end.

Definition CountBinders (e : Expr) : nat := count_binders (e _).

Class Context (Name : Type) (var : Type) :=
  { ContextT : Type;
    extendb : ContextT -> Name -> var -> ContextT;
    empty : ContextT }.
Coercion ContextT : Context >-> Sortclass.
Arguments ContextT {_ _ _}, {_ _} _.
Arguments extendb {_ _ _} _ _ _.
Arguments empty {_ _ _}.

Module Export Named.
Inductive expr Name : Type :=
| Const : expr Name
| LetIn : Name -> expr Name -> expr Name -> expr Name.
End Named.

Global Arguments Const {_}.
Global Arguments LetIn {_} _ _ _.

Definition split_onames {Name : Type} (ls : list (option Name))
  : option (Name) * list (option Name)
  := match ls with
          | cons n ls'
            => (n, ls')
          | nil => (None, nil)
     end.

Section internal.
  Context (InName OutName : Type)
          {InContext : Context InName (OutName)}
          {ReverseContext : Context OutName (InName)}
          (InName_beq : InName -> InName -> bool).

  Fixpoint register_reassign (ctxi : InContext) (ctxr : ReverseContext)
           (e : expr InName) (new_names : list (option OutName))
    : option (expr OutName)
    := match e in Named.expr _ return option (expr _) with
       | Const => Some Const
       | LetIn n ex eC
         => let '(n', new_names') := eta (split_onames new_names) in
            match n', @register_reassign ctxi ctxr ex nil with
            | Some n', Some x
              => let ctxi := @extendb _ _ _ ctxi n n' in
                 let ctxr := @extendb _ _ _ ctxr n' n in
                 option_map (LetIn n' x) (@register_reassign ctxi ctxr eC new_names')
            | None, Some x
              => let ctxi := ctxi in
                 @register_reassign ctxi ctxr eC new_names'
            | _, None => None
            end
       end.

End internal.

Global Instance pos_context (var : Type) : Context positive var
  := { ContextT := PositiveMap.t var;
       extendb ctx key v := PositiveMap.add key v ctx;
       empty := PositiveMap.empty _ }.

Global Arguments register_reassign {_ _ _ _} ctxi ctxr e _.

Section language5.
  Context (Name : Type).

  Local Notation expr := (@Top.expr Name).
  Local Notation nexpr := (@Named.expr Name).

  Fixpoint ocompile (e : expr) (ls : list (option Name)) {struct e}
    : option (nexpr)
    := match e in @Top.expr _ return option (nexpr) with
       | Top.Const => Some Named.Const
       | Top.LetIn ex eC
         => match @ocompile ex nil, split_onames ls with
            | Some x, (Some n, ls')%core
              => option_map (fun C => Named.LetIn n x C) (@ocompile (eC n) ls')
            | _, _ => None
            end
       end.

  Definition compile (e : expr) (ls : list Name) := @ocompile e (List.map (@Some _) ls).
End language5.

Global Arguments compile {_} e ls.

Fixpoint merge_liveness (ls1 ls2 : list unit) :=
  match ls1, ls2 with
  | cons x xs, cons y ys => cons tt (@merge_liveness xs ys)
  | nil, ls | ls, nil => ls
  end.

Section internal1.
  Context (Name : Type)
          (OutName : Type)
          {Context : Context Name (list unit)}.

  Definition compute_livenessf_step
             (compute_livenessf : forall (ctx : Context) (e : expr Name) (prefix : list unit), list unit)
             (ctx : Context)
             (e : expr Name) (prefix : list unit)
    : list unit
    := match e with
       | Const => prefix
       | LetIn n ex eC
         => let lx := @compute_livenessf ctx ex prefix in
            let lx := merge_liveness lx (prefix ++ repeat tt 1) in
            let ctx := @extendb _ _ _ ctx n (lx) in
            @compute_livenessf ctx eC (prefix ++ repeat tt 1)
       end.

  Fixpoint compute_liveness ctx e prefix
    := @compute_livenessf_step (@compute_liveness) ctx e prefix.

  Fixpoint insert_dead_names_gen def (ls : list unit) (lsn : list OutName)
    : list (option OutName)
    := match ls with
       | nil => nil
       | cons live xs
         => match lsn with
            | cons n lsn' => Some n :: @insert_dead_names_gen def xs lsn'
            | nil => def :: @insert_dead_names_gen def xs nil
            end
       end.
  Definition insert_dead_names def (e : expr Name)
    := insert_dead_names_gen def (compute_liveness empty e nil).
End internal1.

Global Arguments insert_dead_names {_ _ _} def e lsn.

Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.

Section language7.
  Context {Context : Context unit (positive)}.

  Local Notation nexpr := (@Named.expr unit).

  Definition CompileAndEliminateDeadCode (e : Expr) (ls : list unit)
    : option (nexpr)
    := let e := compile (Name:=positive) (e _) (List.map Pos.of_nat (seq 1 (CountBinders e))) in
       match e with
       | Some e => Let_In (insert_dead_names None e ls) (* help vm_compute by factoring this out *)
                          (fun names => register_reassign empty empty e names)
       | None => None
       end.
End language7.

Global Arguments CompileAndEliminateDeadCode {_} e ls.

Definition ContextOn {Name1 Name2} f {var} (Ctx : Context Name1 var) : Context Name2 var
  := {| ContextT := Ctx;
        extendb ctx n v := extendb ctx (f n) v;
        empty := empty |}.

Definition Register := Datatypes.unit.

Global Instance RegisterContext {var : Type} : Context Register var
  := ContextOn (fun _ => 1%positive) (pos_context var).

Definition syntax := Named.expr Register.

Definition AssembleSyntax e ls (res := CompileAndEliminateDeadCode e ls)
  := match res return match res with None => _ | _ => _ end with
     | Some v => v
     | None => I
     end.

Definition dummy_registers (n : nat) : list Register
  := List.map (fun _ => tt) (seq 0 n).
Definition DefaultRegisters (e : Expr) : list Register
  := dummy_registers (CountBinders e).

Definition DefaultAssembleSyntax e := @AssembleSyntax e (DefaultRegisters e).

Notation "'slet' x := A 'in' b" := (Top.LetIn A (fun x => b)) (at level 200, b at level 200).
Notation "#[ var ]#" := (@Top.Const var).

Definition compiled_syntax : Expr := fun (var : Type) =>
(
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
  slet x1 := #[ var ]# in
 @Top.Const var).

Definition v :=
  Eval cbv [compiled_syntax] in (DefaultAssembleSyntax (compiled_syntax)).

Timeout 2 Eval vm_compute in v.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


text:
(* Distributed under the terms of the MIT license. *)
From MetaCoq.Utils Require Import utils.
From MetaCoq.Common Require Import config.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICInduction
    PCUICLiftSubst.

Require Import ssreflect.
From Equations Require Import Equations.

(** * Substitution lemmas for typing derivations. *)

Local Set Keyed Unification.

Set Default Goal Selector "!".

#[global]
Hint Rewrite @app_context_length : wf.

Generalizable Variables Σ Γ t T.

(** Linking a context (with let-ins), an instance (reversed substitution)
    for its assumptions and a well-formed substitution for it. *)

Inductive context_subst : context -> list term -> list term -> Type :=
| context_subst_nil : context_subst [] [] []
| context_subst_ass Γ args s na t a :
    context_subst Γ args s ->
    context_subst (vass na t :: Γ) (args ++ [a]) (a :: s)
| context_subst_def Γ args s na b t :
    context_subst Γ args s ->
    context_subst (vdef na b t :: Γ) args (subst s 0 b :: s).
Derive Signature for context_subst.

(** Promoting a substitution for the non-let declarations of ctx into a
    substitution for the whole context *)

Fixpoint make_context_subst ctx args s :=
  match ctx with
  | [] => match args with
          | [] => Some s
          | a :: args => None
          end
  | d :: ctx =>
    match d.(decl_body) with
    | Some body => make_context_subst ctx args (subst0 s body :: s)
    | None => match args with
              | a :: args => make_context_subst ctx args (a :: s)
              | [] => None
              end
    end
  end.

Lemma context_subst_length {Γ a s} : context_subst Γ a s -> #|Γ| = #|s|.
Proof. induction 1; simpl; congruence. Qed.

Lemma context_subst_assumptions_length {Γ a s} : context_subst Γ a s -> context_assumptions Γ = #|a|.
Proof. induction 1; simpl; try congruence. rewrite app_length /=. lia. Qed.

(* Lemma context_subst_app {cf:checker_flags} Γ Γ' a s : *)
(*   context_subst (Γ' ++ Γ) a s -> *)
(*   { a0 & { a1 & { s0 & { s1 & (context_subst Γ a0 s0 * context_subst (subst_context s0 0 Γ') a1 s1 *)
(*                                * (a = a0 ++ a1) * (s = s1 ++ s0))%type } } } }. *)
(* Proof. *)
(*   induction Γ' in Γ, a, s |- *. simpl. *)
(*   exists a, [], s, []. rewrite app_nil_r; intuition. constructor. *)

(*   simpl. intros Hs. *)
(*   inv Hs. *)
(*   - specialize (IHΓ' _ _ _ H). *)
(*     destruct IHΓ' as (a0' & a1' & s1 & s2 & ((sa0 & sa1) & eqargs) & eqs0). *)
(*     subst. exists a0', (a1' ++ [a1]), s1, (a1 :: s2). intuition eauto. *)
(*     rewrite subst_context_snoc. constructor. auto. now rewrite app_assoc. *)
(*   - specialize (IHΓ' _ _ _ H). *)
(*     destruct IHΓ' as (a0' & a1' & s1 & s2 & ((sa0 & sa1) & eqargs) & eqs0). *)
(*     subst. exists a0', a1', s1, (subst s2 0 (subst s1 #|Γ'| b) :: s2). intuition eauto. *)
(*     rewrite -> subst_context_snoc, Nat.add_0_r. *)
(*     unfold subst_decl; simpl. unfold map_decl. simpl. *)
(*     econstructor. auto. simpl. f_equal. *)
(*     rewrite -> subst_app_simpl; auto. simpl. *)
(*     pose proof(context_subst_length _ _ _ sa1) as Hs1. *)
(*     rewrite subst_context_length in Hs1. rewrite -> Hs1. auto. *)
(* Qed. *)

Lemma make_context_subst_rec_spec ctx args s tele args' s' :
  context_subst ctx args s ->
  make_context_subst tele args' s = Some s' ->
  context_subst (List.rev tele ++ ctx) (args ++ args') s'.
Proof.
  induction tele in ctx, args, s, args', s' |- *.
  - move=> /= Hc. case: args'.
    + move => [= <-].
      now rewrite app_nil_r.
    + move=> a l //.
  - move=> Hc /=. case: a => [na [body|] ty] /=.
    -- specialize (IHtele (vdef na body ty :: ctx) args (subst0 s body :: s) args' s').
       move=> /=. rewrite <- app_assoc.
       move/(IHtele _). move=> H /=. apply H.
       constructor. auto.
    -- case: args' => [|a args']; try congruence.
       specialize (IHtele (vass na ty :: ctx) (args ++ [a]) (a :: s) args' s').
       move=> /=. rewrite <- app_assoc.
       move/(IHtele _). move=> H /=. simpl in H. rewrite <- app_assoc in H. apply H.
       constructor. auto.
Qed.

Lemma make_context_subst_spec tele args s' :
  make_context_subst tele args [] = Some s' ->
  context_subst (List.rev tele) args s'.
Proof.
  move/(make_context_subst_rec_spec [] [] [] _ _ _ context_subst_nil).
  rewrite app_nil_r /= //.
Qed.

Lemma subst_telescope_cons s k d Γ :
  subst_telescope s k (d :: Γ) =
  map_decl (subst s k) d :: subst_telescope s (S k) Γ.
Proof.
  simpl.
  unfold subst_telescope, mapi. simpl. f_equal.
  rewrite mapi_rec_Sk. apply mapi_rec_ext.
  intros. simpl. now rewrite Nat.add_succ_r.
Qed.

Lemma subst_telescope_comm_rec s k s' k' Γ:
  subst_telescope (map (subst s' k) s) k' (subst_telescope s' (#|s| + k' + k) Γ) =
  subst_telescope s' (k' + k) (subst_telescope s k' Γ).
Proof.
  induction Γ in k, k' |- *; rewrite ?subst_telescope_cons; simpl; auto.
  f_equal.
  * unfold map_decl. simpl.
    f_equal.
    + destruct a as [na [b|] ty]; simpl; auto.
      f_equal. now rewrite distr_subst_rec.
    + now rewrite distr_subst_rec.
  * specialize (IHΓ k (S k')). now rewrite Nat.add_succ_r in IHΓ.
Qed.

Lemma subst_telescope_comm s k s' Γ:
  subst_telescope (map (subst s' k) s) 0 (subst_telescope s' (#|s| + k) Γ) =
  subst_telescope s' k (subst_telescope s 0 Γ).
Proof.
  now rewrite -(subst_telescope_comm_rec _ _ _ 0) Nat.add_0_r.
Qed.

Lemma decompose_prod_n_assum_extend_ctx {ctx n t ctx' t'} ctx'' :
  decompose_prod_n_assum ctx n t = Some (ctx', t') ->
  decompose_prod_n_assum (ctx ++ ctx'') n t = Some (ctx' ++ ctx'', t').
Proof.
  induction n in ctx, t, ctx', t', ctx'' |- *.
  - simpl. intros [= -> ->]. eauto.
  - simpl.
    destruct t; simpl; try congruence.
    + intros H. eapply (IHn _ _ _ _ ctx'' H).
    + intros H. eapply (IHn _ _ _ _ ctx'' H).
Qed.

Lemma context_subst_length2 {ctx args s} : context_subst ctx args s -> #|args| = context_assumptions ctx.
Proof.
  induction 1; simpl; auto.
  rewrite app_length; simpl; lia.
Qed.

Lemma context_subst_fun {ctx args s s'} : context_subst ctx args s -> context_subst ctx args s' -> s = s'.
Proof.
  induction 1 in s' |- *; intros H'; depelim H'; auto.
  - eapply app_inj_tail in H. intuition subst.
    now specialize (IHX _ H').
  - now specialize (IHX _ H').
Qed.

Lemma context_subst_fun' {ctx args args' s s'} : context_subst ctx args s -> context_subst ctx args' s' -> #|args| = #|args'|.
Proof.
  induction 1 as [ | ? ? ? ? ? ? ? IHX | ? ? ? ? ? ? ? IHX ] in args', s' |- *; intros H'; depelim H'; auto.
  - now rewrite !app_length; specialize (IHX _ _ H').
  - now specialize (IHX _ _ H').
Qed.

#[global] Hint Constructors context_subst : core.

Lemma context_subst_app {ctx ctx' args s} :
  context_subst (ctx ++ ctx') args s ->
  context_subst (subst_context (skipn #|ctx| s) 0 ctx) (skipn (context_assumptions ctx') args) (firstn #|ctx| s) *
  context_subst ctx' (firstn (context_assumptions ctx') args) (skipn #|ctx| s).
Proof.
  revert ctx' args s.
  induction ctx; intros ctx' args s; simpl.
  - intros Hc.
    rewrite - !(context_subst_length2 Hc).
    now rewrite firstn_all skipn_all.
  - intros Hc.
    depelim Hc.
    * rewrite skipn_S.
      specialize (IHctx _ _ _ Hc) as [IHctx IHctx'].
      pose proof (context_subst_length2 IHctx).
      pose proof (context_subst_length2 IHctx').
      pose proof (context_subst_length2 Hc).
      rewrite context_assumptions_app in H1.
      rewrite firstn_app. rewrite (firstn_0 [a0]).
      { rewrite firstn_length_le in H0; lia. }
      rewrite app_nil_r. split; auto.
      rewrite skipn_app_le; try lia.
      rewrite subst_context_snoc.
      now constructor.

    * specialize (IHctx _ _ _ Hc).
      split; try now rewrite skipn_S.
      pose proof (context_subst_length2 Hc).
      rewrite context_assumptions_app in H.
      destruct IHctx as [IHctx _].
      pose proof (context_subst_length IHctx).
      rewrite subst_context_snoc. rewrite !skipn_S.
      rewrite /subst_decl /map_decl /= Nat.add_0_r.
      rewrite -{4}(firstn_skipn #|ctx| s0).
      rewrite subst_app_simpl. simpl.
      rewrite subst_context_length in H0. rewrite -H0.
      now constructor.
Qed.

Lemma make_context_subst_recP ctx args s tele args' s' :
  context_subst ctx args s ->
  (make_context_subst tele args' s = Some s') <~>
  context_subst (List.rev tele ++ ctx) (args ++ args') s'.
Proof.
  induction tele in ctx, args, s, args', s' |- *.
  - move=> /= Hc. case: args'.
    * split.
      + move => [= <-].
        now rewrite app_nil_r.
      + rewrite app_nil_r.
        move/context_subst_fun => Hs. now specialize (Hs _ Hc).
    * intros. split; try discriminate.
      intros H2. pose proof (context_subst_fun' Hc H2).
      rewrite app_length /= in H. now lia.
  - move=> Hc /=. case: a => [na [body|] ty] /=.
    * specialize (IHtele (vdef na body ty :: ctx) args (subst0 s body :: s) args' s').
      move=> /=. rewrite <- app_assoc.
      now forward IHtele by (constructor; auto).
    * destruct args' as [|a args'].
      + split; [congruence | ]. intros Hc'.
        pose proof (context_subst_length2 Hc').
        rewrite !context_assumptions_app ?app_length ?List.rev_length /= Nat.add_0_r in H.
        pose proof (context_subst_length2 Hc). lia.

      + specialize (IHtele (vass na ty :: ctx) (args ++ [a]) (a :: s) args' s').
        forward IHtele. { econstructor. auto. }
        rewrite -app_assoc. rewrite -app_comm_cons /=.
        rewrite -app_assoc in IHtele. apply IHtele.
Qed.

Lemma make_context_subst_spec_inv : forall (tele : list context_decl) (args s' : list term),
  context_subst (List.rev tele) args s' ->
  make_context_subst tele args [] = Some s'.
Proof.
  intros. assert (H:=make_context_subst_recP [] [] [] tele args s').
  forward H by constructor.
  rewrite app_nil_r in H. destruct H.
  simpl in *. auto.
Qed.

Lemma context_subst_subst_extended_subst inst s Δ :
  context_subst Δ inst s ->
  s = map (subst0 (List.rev inst)) (extended_subst Δ 0).
Proof using Type.
  intros sp.
  induction sp.
  - simpl; auto.
  - rewrite List.rev_app_distr /= lift0_id. f_equal.
    rewrite lift_extended_subst.
    rewrite map_map_compose. rewrite IHsp. apply map_ext.
    intros. rewrite (subst_app_decomp [_]). f_equal.
    simpl. rewrite simpl_subst ?lift0_id //.
  - simpl. len.
    f_equal; auto.
    rewrite IHsp.
    rewrite distr_subst. f_equal.
    simpl; len.
    pose proof (context_subst_length2 sp).
    rewrite -H. rewrite -(List.rev_length args).
    rewrite -(Nat.add_0_r #|List.rev args|).
    rewrite simpl_subst_rec; try lia.
    now rewrite lift0_id.
Qed.

From MetaCoq.PCUIC Require Import PCUICSigmaCalculus.

(**************************)
(* Section  mk_ctx_subst  *)
(**************************)

Lemma context_subst_subst_expand_lets inst s Δ t k :
  context_subst Δ inst s ->
  subst s k t = subst (List.rev inst) k (expand_lets_k Δ k t).
Proof.
  move=> /[dup] H /context_subst_subst_extended_subst ->.
  apply: map_subst_expand_lets_k.
  rewrite List.rev_length.
  apply: context_subst_assumptions_length; eassumption.
Qed.

Lemma make_context_subst_context_assumptions Δ args s :
  context_assumptions Δ = #|args| ->
  ∑ s', make_context_subst Δ args s = Some s'.
Proof.
  elim: Δ args s=> [|[?[?|]?] Δ ih].
  + move=> []//=;eexists; reflexivity.
  + move=> /= ??; apply:ih.
  + move=> /= [//|hd tl /=] s [=]. apply: ih.
Qed.

Definition mk_ctx_subst Δ args := option_get [] (make_context_subst (List.rev Δ) args []).

Lemma mk_ctx_subst_spec {Δ args} :
  context_assumptions Δ = #|args| ->
  context_subst Δ args (mk_ctx_subst Δ args).
Proof.
  rewrite /mk_ctx_subst -context_assumptions_rev.
  move=> /(make_context_subst_context_assumptions _ _ []) [? /[dup] ? ->] /=.
  rewrite -[Δ]rev_involutive.
  by apply: make_context_subst_spec.
Qed.

Lemma mk_ctx_subst_length Δ l :
  context_assumptions Δ = #|l| -> #|mk_ctx_subst Δ l| = #|Δ|.
Proof.
  move=> /mk_ctx_subst_spec /context_subst_length //.
Qed.

From Coq Require Import ssrbool.
From MetaCoq.PCUIC Require Import PCUICClosed.
Lemma closedn_ctx_subst_forall n Δ l s :
  context_subst Δ l s ->
  closedn_ctx n Δ ->
  forallb (closedn n) l ->
  forallb (closedn n) s.
Proof.
  move=> z; depind z=> //= /andP[/=? d].
  - rewrite forallb_app=> /andP[?] /andP[/= -> _] /=; by apply: IHz.
  - move=> ?.
    have ? : forallb (closedn n) s by apply: IHz.
    apply/andP; split=> //; apply: closedn_subst0=> //.
    move: d=> /andP /= []; rewrite (context_subst_length z) Nat.add_comm //.
Qed.

author: MetaCoq

repo: metacoq

save_path: github-repos/coq/MetaCoq-metacoq


text:
From Hammer Require Import Hammer.

Require Import List.
From hahn Require Import HahnBase.
Set Implicit Arguments.

Section FunctionUpdate.

Variables (A B: Type).

Definition upd (f : A -> B) a b x :=
if excluded_middle_informative (x = a) then b else f x.

Lemma upds f a b : upd f a b a = b.
Proof. hammer_hook "HahnFun" "HahnFun.upds". unfold upd; desf. Qed.

Lemma updo f a b c (NEQ: c <> a) : upd f a b c = f c.
Proof. hammer_hook "HahnFun" "HahnFun.updo". unfold upd; desf. Qed.

Lemma updss f l x y : upd (upd f l x) l y = upd f l y.
Proof. hammer_hook "HahnFun" "HahnFun.updss".
extensionality z; unfold upd; desf.
Qed.

Lemma updC l l' (NEQ: l <> l') f x y :
upd (upd f l x) l' y = upd (upd f l' y) l x.
Proof. hammer_hook "HahnFun" "HahnFun.updC".
extensionality z; unfold upd; desf.
Qed.

Lemma updI f a : upd f a (f a) = f.
Proof. hammer_hook "HahnFun" "HahnFun.updI".
extensionality a'; unfold upd; desf.
Qed.

Lemma map_upd_irr a l (NIN: ~ In a l) f b :
map (upd f a b) l = map f l.
Proof. hammer_hook "HahnFun" "HahnFun.map_upd_irr".
unfold upd; induction l; ins.
apply not_or_and in NIN; desf; f_equal; eauto.
Qed.

End FunctionUpdate.

Ltac rupd := repeat first [rewrite upds | rewrite updo ; try done].

Section DecidableUpdate.

Variables (A: eqType) (B: Type).

Definition mupd (f: A -> B) y z :=
fun x => if eq_op x y then z else f x.

Lemma mupds f x y : mupd f x y x = y.
Proof. hammer_hook "HahnFun" "HahnFun.mupds". by unfold mupd; desf; desf. Qed.

Lemma mupdo f x y z : x <> z -> mupd f x y z = f z.
Proof. hammer_hook "HahnFun" "HahnFun.mupdo". by unfold mupd; desf; desf. Qed.

Lemma mupdss f l x y : mupd (mupd f l x) l y = mupd f l y.
Proof. hammer_hook "HahnFun" "HahnFun.mupdss".
extensionality z; unfold mupd; desf; desf.
Qed.

Lemma mupdC l l' (NEQ: l <> l') f x y :
mupd (mupd f l x) l' y = mupd (mupd f l' y) l x.
Proof. hammer_hook "HahnFun" "HahnFun.mupdC".
extensionality z; unfold mupd; desf; desf.
Qed.

Lemma mupdI f a : mupd f a (f a) = f.
Proof. hammer_hook "HahnFun" "HahnFun.mupdI".
extensionality z; unfold mupd; desf; desf.
Qed.

Lemma map_mupd_irr a l (NIN: ~ In a l) f b :
map (mupd f a b) l = map f l.
Proof. hammer_hook "HahnFun" "HahnFun.map_mupd_irr".
unfold mupd; induction l; ins.
apply not_or_and in NIN; desf; desf; f_equal; eauto.
Qed.

End DecidableUpdate.

Arguments mupd [A B] f y z x.

author: lukaszcz

repo: coqhammer-eval


text:
From Perennial.goose_lang Require Import notation typing.

Module lock.
  Section goose_lang.
    Context {ext:ffi_syntax}.

    Local Coercion Var' (s:string): expr := Var s.

    Definition new: val := λ: <>, ref #false.
    Definition try_acquire : val := λ: "l", CAS "l" #false #true.
    Definition acquire : val :=
      rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
    Definition release : val := λ: "l", CmpXchg "l" #true #false;; #().

    (* XXX: let binding so we can do an iMod after the allocation *)
    Definition newCond: val := λ: "l", let: "cond" := ref "l" in "cond".
    (* no-op in the model, only affects scheduling *)
    Definition condSignal: val := λ: "l", #().
    Definition condBroadcast: val := λ: "l", #().
    Definition condWait: val := λ: "l", release !"l";;
                                        (* actual cond var waits for a signal
                                           here, but the model does not take this
                                           into account *)
                                        acquire !"l".
    Definition condWaitTimeout: val := λ: "l" "timeout", condWait "l".
  End goose_lang.
End lock.

author: mit-pdos

repo: perennial

save_path: github-repos/coq/mit-pdos-perennial


text:
(** Generated by coq-of-ocaml *)
Require Import OCaml.OCaml.

Local Set Primitive Projections.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Unset Positivity Checking.
Unset Guard Checking.

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Inductive natural : Set :=
| Zero : natural
| Succ : natural -> natural.

Fixpoint plus (plus_arg0 : natural) (plus_arg1 : natural) {struct plus_arg0}
  : natural :=
  match plus_arg0 with
  | Zero => plus_arg1
  | Succ n => Succ (plus n plus_arg1)
  end.

Fixpoint mult (mult_arg0 : natural) (mult_arg1 : natural) {struct mult_arg0}
  : natural :=
  match mult_arg0 with
  | Zero => Zero
  | Succ n => plus (mult n mult_arg1) mult_arg1
  end.

Definition synth (y : natural) (x : natural) : natural :=
  plus Zero (mult (Succ x) (Succ y)).

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
Require Import HoTT.
Require Import Pushforwards.

Generalizable Variables T F A B.

Local Notation Endofunctor := (Type -> Type).

Class TFunctor (F: Endofunctor) :=
  fmap: forall {A B: Type}, (A -> B) -> (F A -> F B).

Arguments fmap F {_} A B _ _.
Global Notation "f $ a" := (fmap f _ _ a) (at level 99, right associativity).

Class TApplicative `{TFunctor T} := {
  pure: forall {A: Type}, A -> T A;
  fzip: forall {A B: Type}, T (A -> B) -> T A -> T B
  }.

Arguments TApplicative T [_].
Arguments pure T [_ _ A] _.
Arguments fzip T [_ _] A B _ _.

Class TMonad (T: Endofunctor) := {
  bind: forall {A B: Type}, (T A) -> (A -> T B) -> T B;
  ret: forall {A: Type}, A -> T A
  }.

Notation "x >>= f" := (bind x f) (at level 90).
Notation "x <- y ; f" := (y >>= (fun x => f))
    (at level 100, f at level 200,
    format "'[v' x  '<-'  y ';' '/' f ']'").

Section Monads.

  Context `{TMonad T}.

  Global Instance monad_is_functor: TFunctor T :=
    fun `(f: A -> B) (t: T A) => x <- t; ret (f x).

  Definition join {A: Type} (t: T (T A)): T A
    := x <- t; x.

  Lemma join_is_action (A: Type):
    join o (T $ join) = join o (join (A:=T A)).
  Admitted.

  Lemma ret_is_unit (A: Type) (x: T A): join ((T $ ret) x) = x.
  Admitted.

  Global Instance monad_is_applicative: TApplicative T
    := let Tapply A B := fun (f: T (A -> B)) (t: T A) =>
    a <- t; g <- f; ret (g a)
    in {| pure := @ret _ _; fzip := fun A B => Tapply  A B |}.

End Monads.

Section Algebras.

  Context `{TMonad T}.
  Variable T_act: T Type -> Type.

  Section Composition.

    Context {A: Type}.
    Variable is_op : (T A -> A) -> Type.

    (** Morally a point in this type corresponds to T h, where h is some virtual operation. In the case T = List such points are lists [f_1, .. , f_k] of operations with arities [n_1, .. , n_k]. *)
    Definition T_is_op: (T (T A) -> T A) -> Type :=
      let t_fam := T_act o (T $ is_op)
      in push_sigma t_fam (fzip T _ _).

    Definition VirtualCompose :=
      forall (f: sig T_is_op) (g: sig is_op),
      { h: sig is_op | h.1 o join = g.1 o f.1 }.

    Definition VirtualUnit :=
      forall (f: sig is_op), f.1 o ret = idmap.

  End Composition.

  Record TAlgebra (A: Type):=
  {
    is_op: (T A -> A) -> Type;
    comp: VirtualCompose is_op;
    unit: VirtualUnit is_op;
    unique_op: Contr (sig is_op)
    }.

  Arguments is_op {A} _ _.
  Arguments comp {A} _ _ _.
  Arguments unit {A} _ _.
  Arguments unique_op {A} _.

  Theorem unique_compose {X: Type} {A: TAlgebra X}
        (f: sig (T_is_op A.(is_op)))  (g: sig A.(is_op))
        (R S: VirtualCompose A.(is_op)): R f g = S f g.
    unfold VirtualCompose in R, S.
    pose (Rx := R f g).
    pose (Sx := S f g).
    assert (Rx = Sx).
    destruct Rx as [?h ?p], Sx as [?h ?p].
    destruct A.

author: afetisov

repo: HottCat

save_path: github-repos/coq/afetisov-HottCat


text:
(** instantiates the scheme from [GenMendlerIteration_alt] for use in the analysis of recursion schemes involving
    actegories (hence, with actions of monoidal categories on categories)

author: Ralph Matthes, 2023
*)

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.limits.initial.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.Chains.Chains.
Require Import UniMath.CategoryTheory.Chains.Adamek.
Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors.
Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Actegories.Actegories.
Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories.
Require Import UniMath.CategoryTheory.Actegories.CoproductsInActegories.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.SubstitutionSystems.GenMendlerIteration_alt.
Require Import UniMath.SubstitutionSystems.GeneralizedSubstitutionSystems.

Local Open Scope cat.

Import BifunctorNotations.
Import ActegoryNotations.

Section FixAnActegory.

  Context {V : category} (Mon_V : monoidal V) {C : category}
    (IC : Initial C) (CC : Colims_of_shape nat_graph C)
    (Act : actegory Mon_V C)
    (v : V).

Section FixAFunctor.

  Context (F : functor C C) (HF : is_omega_cocont F).

  Let AF : category := FunctorAlg F.
  Let chnF : chain C := initChain IC F.
  Let μF_Initial : Initial AF := colimAlgInitial IC HF (CC chnF).
  Let μF : C := alg_carrier _ (InitialObject μF_Initial).
  Let α : F μF --> μF := alg_map F (pr1 μF_Initial).

  Context (y : C) (G : functor C C) (ρ' : G y --> y).

  Let L : functor C C := leftwhiskering_functor Act v.

  Context (IL : isInitial C (v ⊗_{Act} (InitialObject IC))) (HL : is_omega_cocont L).

  Definition SpecialGenMendlerIterationWithActegory (θ' : F ∙ L ⟹ L ∙ G) :
    ∃! h : v ⊗_{Act} μF --> y, v ⊗^{Act}_{l} α · h = θ' μF · #G h · ρ'
    := SpecialGenMendlerIteration IC CC F HF y L IL HL G ρ' θ'.

End FixAFunctor.

Section Const_H_AsFunctor.

  Context (CP : BinCoproducts C).

  Context (H : functor C C) (HH : is_omega_cocont H) (c0 : C).

  Let Const_plus_H (c : C) : functor C C := GeneralizedSubstitutionSystems.Const_plus_H H CP c.

  Let AF : category := FunctorAlg (Const_plus_H c0).
  Let chnF : chain C := initChain IC (Const_plus_H c0).

  Local Lemma HF : is_omega_cocont (Const_plus_H c0).
  Proof.
    apply is_omega_cocont_BinCoproduct_of_functors.
    - apply is_omega_cocont_constant_functor.
    - exact HH.
  Qed.

  Let μF_Initial : Initial AF := colimAlgInitial IC HF (CC chnF).
  Let μF : C := alg_carrier _ (InitialObject μF_Initial).
  Let α : Const_plus_H c0 μF --> μF := alg_map (Const_plus_H c0) (pr1 μF_Initial).

  Let η : constant_functor C C c0 μF --> μF := BinCoproductIn1 (CP _ _) · α.
  Let τ : H μF --> μF := BinCoproductIn2 (CP _ _) · α.

  Context (y : C) (θ : lineator_lax Mon_V Act Act H) (ρ : H y --> y) (f : v ⊗_{Act} c0 --> y).

  Context (IL : isInitial C (v ⊗_{Act} (InitialObject IC))).

  Let L : functor C C := leftwhiskering_functor Act v.

  Context (HL : is_omega_cocont L).

  Definition charprop_SpecialGenMendlerIterationWithActegoryAndStrength (h : C ⟦v ⊗_{Act} μF, y⟧) : UU :=
    v ⊗^{Act}_{l} η · h = f × v ⊗^{Act}_{l} τ · h = θ v μF · #H h · ρ.

  Lemma isaprop_charprop_SpecialGenMendlerIterationWithActegoryAndStrength (h : C ⟦v ⊗_{Act} μF, y⟧) :
    isaprop (charprop_SpecialGenMendlerIterationWithActegoryAndStrength h).
  Proof.
    apply isapropdirprod; apply C.
  Qed.

  Definition singleeq_SpecialGenMendlerIterationWithActegoryAndStrength (h : C ⟦v ⊗_{Act} μF, y⟧) : UU :=
    actegory_bincoprod_antidistributor Mon_V CP Act _ _ _ · v ⊗^{Act}_{l} α · h =
                                     BinCoproductArrow (CP _ _) f (θ v μF · #H h · ρ).

  Context (δ : actegory_bincoprod_distributor Mon_V CP Act).

  Definition instance_SpecialGenMendlerIterationWithActegory (h : C ⟦v ⊗_{Act} μF, y⟧) : UU :=
    v ⊗^{Act}_{l} α · h = δ v c0 (H μF) · BinCoproductOfArrows _ (CP _ _) (CP _ _) f (θ v μF) ·
                            #(Const_plus_H y) h · BinCoproductArrow (CP _ _) (identity y) ρ.

  Local Lemma charpropequivsingleeq (h : v ⊗_{Act} μF --> y) :
    charprop_SpecialGenMendlerIterationWithActegoryAndStrength h <-> singleeq_SpecialGenMendlerIterationWithActegoryAndStrength h.
  Proof.
    split.
    - intros [Hchar1 Hchar2].
      red.
      use BinCoproductArrowsEq.
      + etrans.
        { repeat rewrite assoc.
          do 2 apply cancel_postcomposition.
          apply BinCoproductIn1Commutes. }
        etrans.
        { apply cancel_postcomposition.
          apply pathsinv0, (functor_comp (leftwhiskering_functor Act v)). }
        etrans.
        { exact Hchar1. }
        apply pathsinv0, BinCoproductIn1Commutes.
      + etrans.
        { repeat rewrite assoc.
          do 2 apply cancel_postcomposition.
          apply BinCoproductIn2Commutes. }
        etrans.
        { apply cancel_postcomposition.
          apply pathsinv0, (functor_comp (leftwhiskering_functor Act v)). }
        etrans.
        { exact Hchar2. }
        apply pathsinv0, BinCoproductIn2Commutes.
    - intro Hsingle.
      red in Hsingle.
      split.
      + apply (maponpaths (fun m => BinCoproductIn1 (CP _ _) · m)) in Hsingle.
        unfold actegory_bincoprod_antidistributor, bifunctor_bincoprod_antidistributor, bincoprod_antidistributor in Hsingle.
        repeat rewrite assoc in Hsingle.
        rewrite BinCoproductIn1Commutes in Hsingle.
        assert (aux := functor_comp (leftwhiskering_functor Act v)
                         (BinCoproductIn1 (CP (constant_functor C C c0 μF) (H μF)))
                         α).
        cbn in aux.
        apply (maponpaths (fun m => m · h)) in aux.
        assert (Hsingle' := aux @ Hsingle).
        clear Hsingle aux.
        rewrite BinCoproductIn1Commutes in Hsingle'.
        exact Hsingle'.
      + apply (maponpaths (fun m => BinCoproductIn2 (CP _ _) · m)) in Hsingle.
        unfold actegory_bincoprod_antidistributor, bifunctor_bincoprod_antidistributor, bincoprod_antidistributor in Hsingle.
        repeat rewrite assoc in Hsingle.
        rewrite BinCoproductIn2Commutes in Hsingle.
        assert (aux := functor_comp (leftwhiskering_functor Act v)
                         (BinCoproductIn2 (CP (constant_functor C C c0 μF) (H μF)))
                         α).
        cbn in aux.
        apply (maponpaths (fun m => m · h)) in aux.
        assert (Hsingle' := aux @ Hsingle).
        clear Hsingle aux.
        rewrite BinCoproductIn2Commutes in Hsingle'.
        exact Hsingle'.
  Qed.

  Local Lemma instanceequivsingle (h : v ⊗_{Act} μF --> y) :
    instance_SpecialGenMendlerIterationWithActegory h <-> singleeq_SpecialGenMendlerIterationWithActegoryAndStrength h.
  Proof.
    split.
    - intro Hinst.
      red in Hinst.
      red.
      rewrite assoc'.
      apply (z_iso_inv_on_right _ _ _ (_,,bincoprod_functor_lineator_strongly Mon_V CP Act δ v (_,,_))).
      etrans.
      { exact Hinst. }
      repeat rewrite assoc'.
      apply maponpaths.
      etrans.
      { apply maponpaths.
        apply precompWithBinCoproductArrow. }
      etrans.
      { apply precompWithBinCoproductArrow. }
      apply maponpaths_2.
      cbn.
      rewrite id_left.
      apply id_right.
    - intro Hsingle.
      red in Hsingle.
      red.
      rewrite assoc' in Hsingle.
      apply (z_iso_inv_to_left _ _ _ (_,,bincoprod_functor_lineator_strongly Mon_V CP Act δ v (_,,_))) in Hsingle.
      etrans.
      { exact Hsingle. }
      repeat rewrite assoc'.
      apply maponpaths.
      etrans.
      2: { apply maponpaths.
           apply pathsinv0, precompWithBinCoproductArrow. }
      etrans.
      2: { apply pathsinv0, precompWithBinCoproductArrow. }
      apply maponpaths_2.
      cbn.
      rewrite id_left.
      apply pathsinv0, id_right.
  Qed.

  Local Definition θ'_data := fun (c : C) => δ v c0 (H c) · BinCoproductOfArrows _ (CP _ _) (CP _ _) f (θ v c).

  Let δll : lineator Mon_V (ProductActegory.actegory_binprod Mon_V Act Act) Act
    (bincoproduct_functor CP) := bincoprod_functor_lineator Mon_V CP Act δ.

  Local Lemma θ'_data_is_nat_trans : is_nat_trans ((Const_plus_H c0) ∙ L) (L ∙ (Const_plus_H y)) θ'_data.
  Proof.
    intros c c' g.
    unfold θ'_data. cbn.
    etrans.
    { rewrite assoc.
      apply cancel_postcomposition.
      apply (lineator_linnatleft _ _ _ _ δll v (_,,_) (_,,_) (_,,_)). }
    repeat rewrite assoc'.
    apply maponpaths.
    cbn.
    etrans.
    { apply BinCoproductOfArrows_comp. }
    etrans.
    2: { apply pathsinv0, BinCoproductOfArrows_comp. }
    cbn.
    rewrite (lineator_linnatleft _ _ _ _ θ v).
    apply maponpaths_2.
    etrans.
    { apply cancel_postcomposition.
      apply (functor_id (leftwhiskering_functor Act v)). }
    rewrite id_right.
    apply id_left.
  Qed.

  Local Definition θ' : (Const_plus_H c0) ∙ L ⟹ L ∙ (Const_plus_H y) := _,, θ'_data_is_nat_trans.

  Definition SpecialGenMendlerIterationWithActegoryAndStrength :
    ∃! h : v ⊗_{Act} μF --> y, charprop_SpecialGenMendlerIterationWithActegoryAndStrength h.
  Proof.
    simple refine (iscontrretract _ _ _ (SpecialGenMendlerIterationWithActegory
                                           (Const_plus_H c0) HF y (Const_plus_H y)
                                           (BinCoproductArrow (CP _ _) (identity y) ρ) IL HL θ')).
    - intros [h Hyp].
      exists h.
      apply charpropequivsingleeq.
      apply instanceequivsingle.
      exact Hyp.
    - intros [h Hyp].
      exists h.
      apply charpropequivsingleeq in Hyp.
      apply instanceequivsingle in Hyp.
      exact Hyp.
    - intros [h Hyp].
      use total2_paths_f.
      + apply idpath.
      + apply isaprop_charprop_SpecialGenMendlerIterationWithActegoryAndStrength.
  Defined.

End Const_H_AsFunctor.

End FixAnActegory.

author: UniMath

repo: UniMath

save_path: github-repos/coq/UniMath-UniMath