text:
Require Export Coq.Lists.List.
Require Import Coq.Program.Equality.
Require Import core (* core_axioms *) fintype (* fintype_axioms *).
Import ScopedNotations.
From Chapter10 Require Export sysf_pat.
Require Import Coq.Program.Tactics.

Open Scope fscope.

Ltac inv H := inversion H; try clear H; try subst.

Ltac autorevert x :=
  try (match goal with
    | [y : ?Y |- ?claim] =>
      try (match x with y => idtac end; fail 1);
        match goal with [z : _ |- _] =>
          match claim with context[z] =>
            first
              [ match Y with context[z] => revert y; autorevert x end
              | match y with z => revert y; autorevert x end]
          end
        end
       end).

Definition ctx n := fin n -> ty n.
Definition dctx m n := fin m -> ty n.
Definition empty {X} : fin 0 -> X :=  fun x => match x with end.

Inductive unique {X} : list (nat * X) -> Prop :=
| unil : unique nil
| ucons l x xs : unique xs -> (forall x, ~ In (l, x) xs) ->  unique (cons (l,x) xs).

Hint Constructors unique.

Lemma unique_map {X Y: Type} {f : X -> Y} (xs : list (nat * X)) :
  unique xs -> unique (map (prod_map (fun x => x) f) xs).
Proof.
  intros.
  induction H; cbn; eauto.
  constructor; eauto.
  intros z A. rewrite in_map_iff in A. destruct A as ((?&?)&?&?).
  inv H1. eapply H0; eauto.
Qed.

Lemma unique_spec {X} (xs : list (nat * X)) :
  unique xs -> (forall l x y, In (l, x) xs -> In (l, y) xs -> x = y).
Proof.
  induction 1; intros; cbn in *.
  - contradiction.
  - destruct H1 as [|]; destruct H2 as [|]; try inversion H1; try inversion H2; subst; eauto; firstorder.
Qed.

Lemma in_map {X Y: Type} {f : X -> Y} (xs : list (nat * X)) l x:
  In (l, x) xs -> In (l, f x) (map (prod_map (fun x => x) f) xs).
Proof.
  unfold prod_map.
  induction xs;  cbn; eauto.
  - destruct a; eauto. intros [|]; eauto. inversion H; eauto.
Qed.

Definition label_equiv {X Y} (xs : list (nat * X)) (ys : list (nat * Y)) :=
   (forall i, (exists s, In (i, s) xs) <-> (exists A, In (i, A) ys)).

Lemma label_equiv_map {X X' Y Y': Type} {f : X -> X'} {g : Y -> Y'} (xs : list (nat * X)) (ys : list (nat * Y)) :
  label_equiv xs ys -> label_equiv (map (prod_map (fun x => x) f) xs) (map (prod_map (fun x => x) g) ys).
Proof.
  intros H. intros l.
  unfold prod_map. split; intros (?&?).
  - rewrite in_map_iff in H0. destruct H0 as ((?&?)&?&?). inv H0.
  unfold label_equiv in H. specialize (H l). assert (exists x0, In (l, x0) xs) by eauto.
  apply H in H0. destruct H0 as (?&?). exists (g x). rewrite in_map_iff. exists (l, x). eauto.
- rewrite in_map_iff in H0. destruct H0 as ((?&?)&?&?). inv H0.
  unfold label_equiv in H. specialize (H l). assert (exists x0, In (l, x0) ys) by eauto.
  apply H in H0. destruct H0 as (?&?). exists (f x). rewrite in_map_iff. exists (l, x). eauto.
Qed.

Hint Resolve unique_map label_equiv_map.

Definition update {X} (ts : list (nat * X)) l x : list (nat * X) :=
  map (fun p => if (Nat.eqb (fst p) l) then (l, x) else p) ts.

Lemma unique_update {X} (xs :list (nat * X)) l x :
  unique xs -> unique (update xs l x).
Proof.
  unfold update. intros H.
  induction xs; eauto. inv H. specialize (IHxs H2). cbn.
  destruct (Nat.eqb l0 l) eqn: H; cbn; eauto.
  - constructor; eauto. intros. apply PeanoNat.Nat.eqb_eq in H. subst. intros HH. apply in_map_iff in HH. destruct HH as (?&?&?). destruct x2. cbn in *.  destruct (Nat.eqb n l) eqn: HHH; eauto.
    apply PeanoNat.Nat.eqb_eq in HHH. subst. inv H. eapply H3. eauto. inv H. eapply H3. eauto.
  - constructor; eauto. intros z HH. apply in_map_iff in HH. destruct HH as ((?&?)&?&?). cbn in *.
    destruct (Nat.eqb n l) eqn:HHH; inversion H0; eauto. subst. apply PeanoNat.Nat.eqb_eq in HHH. subst. eapply H3. eauto. subst. eapply H3; eauto.
Qed.

Lemma natequiv_update {X Y} (xs :list (nat * X)) l x (ys: list (nat * Y)):
  label_equiv xs ys -> label_equiv (update xs l x) ys.
Proof.
  enough (label_equiv xs (update xs l x)).
  - intros A i. unfold label_equiv in H, A. now rewrite <- A, H.
  - clear ys. unfold label_equiv. induction xs; cbn; eauto.
    + intros _. split; eauto.
    + destruct a. intros i. cbn. split.
      * intros (?&?). destruct H; eauto.
        -- inv H. destruct (Nat.eqb i l) eqn:HH; eauto. apply PeanoNat.Nat.eqb_eq in HH. subst. eauto. -- assert (exists s, In (i, s) xs) by eauto. apply IHxs in H0. destruct H0 as (?&?). eauto.
      * intros (?&?). destruct H.
        -- destruct (Nat.eqb n l) eqn:HH; eauto. apply PeanoNat.Nat.eqb_eq in HH. subst. inv H. eauto.
        -- assert (exists A, In (i, A) (update xs l x)) by eauto. apply IHxs in H0.
           destruct H0. eauto.
Qed.

Lemma update_char {X} (xs : list (nat * X)) l x i s:
  In (i, s) (update xs l x) -> In (i, s) xs \/ (l = i /\ s = x).
Proof.
  induction xs; eauto. destruct a. cbn.
  destruct (Nat.eqb n l); intros [|]; try inversion H; eauto.
  all: destruct (IHxs H); eauto.
Qed.

Lemma list_dec {X} (P Q : X -> Prop) xs (IH : forall x, In x xs -> P x \/ Q x) :
  (forall x, In x xs -> P x) \/ (exists x, In x xs /\ Q x).
Proof.
  induction xs; cbn; eauto.
  - left. cbn. intros _ [].
  - cbn in IH. assert (forall x, In x xs -> P x \/ Q x) by firstorder.
    destruct (IHxs H) as [|(x&?&?)].
    + assert (P a \/ Q a) as[|] by eauto; cbn; eauto. left. intros z [->|]; cbn; eauto.
    + right. cbn. eauto.
Qed.

Hint Resolve unique_update natequiv_update.

(** POPLMark 1B. *)
Reserved Notation "'SUB' Delta |- A <: B" (at level 68, A at level 99, no associativity).

Inductive sub {n} (Delta : ctx n) : ty n -> ty n -> Prop :=
| SA_top A :
    SUB Delta |- A <: top
| SA_Refl x :
    SUB Delta |- var_ty x <: var_ty x
| SA_Trans x  B :
     SUB Delta |- (Delta x) <: B ->  SUB Delta |- var_ty x <: B
| SA_arrow A1 A2 B1 B2 :
    SUB Delta |- B1 <: A1 -> SUB Delta |- A2 <: B2 ->
    SUB Delta |- arr A1 A2 <: arr B1 B2
| SA_all (A1: ty n) (A2: ty (S n)) B1 B2 :
    SUB Delta |- B1 <: A1 -> @sub (S n) ((B1 .:  Delta) >> ⟨↑⟩) A2 B2 ->
    SUB Delta |- all A1 A2 <: all B1 B2
| SA_rec (xs ys : list (nat * ty n)) : (forall l T', In (l, T') ys -> exists T, In (l, T) xs /\ SUB Delta |- T <: T') ->
                       unique xs -> unique ys -> SUB Delta |- recty xs <: recty ys
where "'SUB' Delta |- A <: B" := (sub Delta A B).

Hint Constructors sub.

Require Import Setoid Morphisms.
Instance sub_morphism {n}:
  Proper (pointwise_relation _ eq ==> eq ==> eq ==> Basics.impl) (@sub n).
Proof.
    (* TODO I think here I actually need a stronger induction lemma though I'm not sure how to do it with two lists. Marcel's Bachelor thesis can probably help *)
Admitted.

Lemma sub_rec :  forall P : forall n : nat, ctx n -> ty n -> ty n -> Prop,
       (forall (n : nat) (Delta : ctx n) (A : ty n), P n Delta A top) ->
       (forall (n : nat) (Delta : ctx n) (x : fin n), P n Delta (var_ty x) (var_ty x)) ->
       (forall (n : nat) (Delta : ctx n) (x : fin n) (B : ty n),
        SUB Delta |- Delta x <: B -> P n Delta (Delta x) B -> P n Delta (var_ty x) B) ->
       (forall (n : nat) (Delta : ctx n) (A1 A2 B1 B2 : ty n),
        SUB Delta |- B1 <: A1 ->
        P n Delta B1 A1 ->
        SUB Delta |- A2 <: B2 -> P n Delta A2 B2 -> P n Delta (arr A1 A2) (arr B1 B2)) ->
       (forall (n : nat) (Delta : ctx n) (A1 : ty n) (A2 : ty (S n)) (B1 : ty n) (B2 : ty (S n)),
        SUB Delta |- B1 <: A1 ->
        P n Delta B1 A1 ->
        SUB (B1 .: Delta) >> ⟨↑⟩ |- A2 <: B2 ->
        P (S n) ((B1 .: Delta) >> ⟨↑⟩) A2 B2 -> P n Delta (all A1 A2) (all B1 B2)) ->
       (forall (n : nat) (Delta : ctx n) (xs ys : list (nat * ty n)),
        (forall (i : nat) (T' : ty n),
         In (i, T') ys -> exists  (T : ty n), In (i, T) xs /\ SUB Delta |- T <: T' /\ P _ Delta T T') ->
        unique xs -> unique ys -> P n Delta (recty xs) (recty ys)) ->
       forall (n : nat) (Delta : ctx n) (t t0 : ty n), SUB Delta |- t <: t0 -> P n Delta t t0.
Proof. intros P. fix IH 11.
  intros. induction H5; try now (clear IH; eauto).
  eapply H4. intros. destruct (H5 _ _ H8) as (T&?&?).
  exists T. repeat split; eauto. all: eauto.
Qed.

Lemma ty_rec
     : forall P : forall nty : nat, ty nty -> Prop,
       (forall (nty : nat) (f : fin nty), P nty (var_ty f)) ->
       (forall nty : nat, P nty top) ->
       (forall (nty : nat) (t : ty nty), P nty t -> forall t0 : ty nty, P nty t0 -> P nty (arr t t0)) ->
       (forall (nty : nat) (t : ty nty),
        P nty t -> forall t0 : ty (S nty), P (S nty) t0 -> P nty (all t t0)) ->
       (forall (nty : nat) (l : list (nat * ty nty)), (forall i t, In (i,t) l -> P _ t) -> P nty (recty l)) ->
       forall (nty : nat) (t : ty nty), P nty t.
Proof.
  intros P. fix IH 7. intros.
  induction t; try now (clear IH; eauto).
  eapply H3. intros. induction l.
  - contradiction.
  - destruct H4 as [|].
    + destruct a. specialize (IH H H0 H1 H2 H3 _ t0). intros. inv H4. apply IH.
    + now apply IHl.
Qed.

Section Pattern.

(** We assume that the subtyping relation is reflexive.
A proof requires a well-formedness condition.*)
Variable sub_refl : forall  n (Delta : ctx n) A, SUB Delta |- A <: A.

Lemma sub_weak m n (Delta1: ctx m) (Delta2: ctx n) A1 A2 A1' A2' (xi: fin m -> fin n) :
  SUB Delta1 |- A1 <: A2 ->
 (forall x, (Delta1 x)⟨xi⟩ = Delta2 (xi x)) ->
  A1' = A1⟨xi⟩ -> A2' = A2⟨xi⟩ ->
  SUB Delta2 |- A1' <: A2' .
Proof.
  intros H. autorevert H. induction H using @sub_rec; intros; subst; asimpl; cbn; econstructor; eauto.
  - eapply IHsub2; try reflexivity.
    auto_case; eauto. rewrite <- H1. now asimpl.
    (* TODO auto_case problems *)
    now asimpl.
  - intros l T' HH. rewrite in_map_iff in HH. destruct HH as ([]&HH&?).
    inv HH. destruct (H _ _ H3) as (?&?&?&?).
    exists (x⟨xi⟩). split; eauto. apply in_map; eauto.
 Qed.

Lemma sub_weak1 n (Delta : ctx n) A A' B B' C :
  SUB Delta |- A <: B ->  A' = A⟨↑⟩ ->  B' = B⟨↑⟩ -> SUB ((C .: Delta) >> ⟨↑⟩) |- A' <: B'.
Proof. intros. eapply sub_weak;  eauto. intros x. now asimpl. Qed.

Definition transitivity_at {n} (B: ty n) := forall m Gamma (A : ty m) C  (xi: fin n -> fin m),
  SUB Gamma |- A <: B⟨xi⟩ -> SUB Gamma |- B⟨ xi⟩ <: C ->  SUB Gamma |- A <: C.

Lemma transitivity_proj n (Gamma: ctx n) A B C :
  transitivity_at B ->
  SUB Gamma |- A <: B -> SUB Gamma |- B <: C -> SUB Gamma |- A <: C.
Proof. intros H. specialize (H n Gamma A C id).  now asimpl in H. Qed.

Hint Resolve transitivity_proj.

Lemma transitivity_ren m n B (xi: fin m -> fin n) : transitivity_at B -> transitivity_at B⟨xi⟩.
Proof. unfold transitivity_at. intros. eapply H with (xi:=funcomp xi0 xi); asimpl in H0; asimpl in H1; eauto. Qed.

Lemma sub_narrow n (Delta Delta': ctx n) A C :
  (forall x, SUB Delta' |- Delta' x <: Delta x) ->
  (forall x, Delta x = Delta' x \/ transitivity_at (Delta x)) ->
  SUB Delta |- A <: C -> SUB Delta' |- A <: C.
Proof with asimpl;eauto.
  intros H H' HH. autorevert HH. induction HH using sub_rec; intros; eauto.
  - destruct (H' x); eauto. rewrite H0 in *. eauto.
  - constructor; eauto.
    eapply IHHH2.
    + auto_case; try apply sub_refl.
      eapply sub_weak; try reflexivity.
      2: intros x; reflexivity. apply H.
    + auto_case. destruct (H' f);  eauto using transitivity_ren.
      rewrite H0. now left.
  - econstructor; eauto. intros l T' HH.
    destruct (H _ _ HH) as (T&?&?&?). exists  T.
    split; eauto.
Qed.

Corollary sub_trans' n (B : ty n): transitivity_at B.
Proof with asimpl;eauto.
  unfold transitivity_at.
  autorevert B. induction B using ty_rec; intros...
  - depind H...
  - depind H... depind H0...
  - depind H... depind H1...
  - depind H... depind H1...
    econstructor... clear IHsub0 IHsub3 IHsub1 IHsub2.
    eapply IHB2 with (xi:=upRen_ty_ty xi); eauto.
    + asimpl. eapply sub_narrow; try eapply H0.
      * auto_case.
        eapply sub_weak with (xi := ↑); try reflexivity; eauto.
        (* adrian: as of 7b3472c the goal is already solved by eauto
         TODO find out why *)
        (* now asimpl. *)
      * intros [x|]; try cbn; eauto. right. apply transitivity_ren. apply transitivity_ren. eauto.
    + asimpl in H1_0. auto.
  - depind H0... depind H3...
    econstructor; eauto. intros.
    destruct (H5 _ _ H6) as (T&?&?). rewrite in_map_iff in H7.
    destruct H7 as ((?&?)&?&?). inv H7.
    edestruct (H2 l0 (t⟨xi⟩)) as (T&?&?).
    + apply in_map_iff. exists (l0, t). eauto.
    + eauto.
Qed.

Corollary sub_trans n (Delta  : ctx n) A B C:
  SUB Delta |- A <: B -> SUB Delta |- B <: C -> SUB Delta |- A <: C.
Proof. eauto using sub_trans'. Qed.

Lemma sub_substitution m m' (sigma : fin m -> ty m') Delta (Delta': ctx m') A B:
   (forall x ,  SUB Delta' |- sigma x <: (Delta x)[sigma] ) ->
   SUB Delta |- A <: B -> SUB Delta' |- subst_ty sigma A <: subst_ty sigma B.
Proof.
    intros eq H. autorevert H. induction H using sub_rec; try now (econstructor; eauto).
  - intros. asimpl. eapply sub_refl.
  - intros. asimpl. eauto. cbn in *. eauto using sub_trans.
  - intros. asimpl. econstructor; eauto.
    asimpl. eapply IHsub2.
    auto_case; asimpl; cbn; eauto using sub_refl.
    eapply sub_weak; try reflexivity. eapply eq.
    all: try now asimpl.
    (* asimpl in H0. *)
  - intros. asimpl. econstructor; eauto. intros. rewrite in_map_iff in H2. destruct H2 as ((?&?)&?&?).
    inv H2. destruct (H _ _ H3) as (T&?&?&?).
    exists (T[sigma]). split; eauto. apply in_map. eauto.
Qed.

(** POPLMark Challenge 2b *)

Variable pat_ty : forall {m} (p: nat), pat m -> ty m ->  (fin p -> (ty m)) -> Prop.
Variable pat_eval : forall {m n} p, pat m -> tm m n -> (fin p -> (tm m n)) -> Prop.
Variable pat_ty_subst: forall {m n} (sigma: fin m -> ty n) p pt A Gamma, pat_ty m p pt A Gamma -> pat_ty n p (pt[sigma]) (A[sigma]) (Gamma >>  subst_ty sigma).

Instance pat_ty_morphism {m p} :
  Proper (eq ==> eq ==> pointwise_relation _ eq ==> Basics.impl) (@pat_ty m p).
Proof.
Admitted.

Inductive value {m n}: tm m n -> Prop :=
| Value_abs A s : value(abs A s)
| Value_tabs A s : value(tabs A s)
| Value_rec xs : (forall i s, In (i, s) xs -> value s) -> value (rectm xs).

Reserved Notation "'TY' Delta ; Gamma |- A : B"
  (at level 68, A at level 99, no associativity,
   format "'TY'  Delta ; Gamma  |-  A  :  B").

Inductive has_ty {m n} (Delta : ctx m) (Gamma : dctx  n m) : tm m n -> ty m -> Prop :=
| T_Var  x :
    TY Delta;Gamma |- var_tm x : Gamma x
  | T_abs (A: ty m) B (s: tm m (S n)):
    @has_ty m (S n) Delta (A .: Gamma) s B   ->
    TY Delta;Gamma |- abs A s : arr A B
| T_app A B s t: TY Delta;Gamma |- s : arr A B  -> TY Delta;Gamma |- t : A -> TY Delta;Gamma |- app s t : B
| T_tabs A B s : @has_ty (S m) n ((A .: Delta) >> ⟨↑⟩) (Gamma >> ⟨↑⟩) s B -> TY Delta;Gamma |- tabs A s : all A B
| T_Tapp A B A' s B' : TY Delta;Gamma |- s : all A B -> SUB Delta |- A' <: A -> B' = B[A'..] ->  TY Delta;Gamma |- tapp s A' : B'
| T_Rcd xs As : unique xs -> unique As -> label_equiv xs As
                -> (forall i A s, In (i, s) xs -> In (i, A) As -> TY Delta; Gamma |- s : A) -> TY Delta;Gamma |- rectm xs : recty As
| T_Proj xs j A As: TY Delta; Gamma |- xs : recty As -> In (j, A) As -> TY Delta; Gamma |- proj xs j : A
| letpat_ty p (pt: pat m) (s : tm m n) (t: tm m (p + n)) A (B : ty m) (Gamma': fin p -> ty m): has_ty Delta Gamma s A -> pat_ty _ p pt A Gamma' -> @has_ty m (p + n) Delta (scons_p p Gamma' Gamma) t B ->  has_ty Delta Gamma (letpat  p pt s t) B
| T_Sub A B s :
    TY Delta;Gamma |- s : A  -> SUB Delta |- A <: B   ->
    TY Delta;Gamma |- s : B
where "'TY' Delta ; Gamma |- s : A" := (has_ty Delta Gamma s A).

Instance has_ty_morphism {m n} :
  Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> eq ==> eq ==> Basics.impl) (@has_ty m n).
Proof.
Admitted.

Lemma T_Var' {m n} (Delta : ctx m) (Gamma : dctx n m) x :
  forall A, A = Gamma x -> TY Delta;Gamma |- var_tm x : A.
Proof. intros A ->. now econstructor. Qed.

Reserved Notation "'EV' s => t"
  (at level 68, s at level 80, no associativity, format "'EV'  s  =>  t").

Inductive eval {m n} : tm m n -> tm m n -> Prop :=
| E_appabs A s t : EV app (abs A s) t => s[ids; t..]
| E_Tapptabs A s B : EV tapp (tabs A s) B => s[B..; ids]
| E_RecProj  xs j s : In (j, s) xs -> EV (proj (rectm  xs) j) => s
| letpat_eval p (pt : pat m) (s : tm m n) (t : tm m (p + n)) (sigma: fin p -> tm m n) :  pat_eval _ _ p pt s sigma -> eval (letpat  p pt s t) (subst_tm (@var_ty m) (scons_p _ sigma (@var_tm _ _)) t)
| E_appFun s s' t :
     EV s => s' ->
     EV app s t => app s' t
| E_appArg s s' v:
     EV s => s' -> value v ->
     EV app v s => app v s'
| E_TyFun s s' A :
     EV s => s' ->
     EV tapp s A => tapp s' A
| E_Proj s s' j : EV s => s' -> EV (proj s j) => (proj s' j)
| E_Rec l ts t t' : EV t => t' -> In (l,t) ts -> EV (rectm ts) => rectm (update ts l t')                  | E_LetL p pt s s' t : EV s => s' -> EV (letpat p pt s t) => (letpat p pt s'  t)
where "'EV' s => t" := (eval s t).

Instance eval_morphism {m n}:
  Proper (eq ==> eq ==> Basics.impl) (@eval m n).
Proof.
Admitted.

(** Assumptions of progress and typing on patterns. *)
Variable pat_progress : forall p pt s A Gamma, TY empty; empty |- s : A -> pat_ty _ p pt A Gamma -> exists sigma, pat_eval _ _ p pt s sigma.

(** Progress *)

Lemma can_form_arr {s: tm 0 0} {A B}:
  TY empty;empty |- s : arr A B -> value s -> exists C t, s = abs C t.
Proof.
  intros H.
  depind H; intros; eauto.
  all: try now (try destruct x0;  try inversion H1).
 + inversion H0; subst; eauto. inversion x.
Qed.

Lemma can_form_all {s A B}:
  TY empty;empty |- s : all A B -> value s -> exists C t, s = tabs C t.
Proof.
  intros H.
  depind H; intros; eauto.
  all: try now (try destruct x0; try inversion H1).
  + inv H0; subst.  inversion x.  eauto.
Qed.

Lemma can_form_rectm {s A}:
  TY empty;empty |- s : recty A -> value s -> exists xs, s = rectm xs /\ forall l A', In (l, A') A -> exists s', In (l, s') xs.
Proof.
  intros H.
  depind H; intros; eauto.
   all: try now (try destruct x0; try inversion H1).
  + eexists. split; eauto.
    intros. apply H1; eauto.
  +  inv H0; subst; eauto.
     * inversion x.
     * edestruct IHhas_ty as (?&?&?); eauto.
       subst. exists x; split; eauto. intros.
       edestruct (H3 _ _ H0).
       eapply H2. apply H5.
Qed.

Theorem ev_progress s A:
  TY empty;empty |- s : A -> value s \/ exists t,  EV s => t.
Proof.
  intros. depind H; eauto; try now (left; constructor).
   - inversion x.
   - right. edestruct IHhas_ty1 as [? | [? ?]]; try reflexivity; eauto.
    + edestruct (can_form_arr H H1) as [? [? ?]]; subst.
      eexists. econstructor.
    + eexists. econstructor. eauto.
  - right. edestruct IHhas_ty as [? | [? ?]]; try reflexivity; eauto.
    + edestruct (can_form_all H H1) as [? [? ?]]; subst. eexists. econstructor.
    + eexists. econstructor. eauto.
  - assert ((forall p, In p xs -> value (snd p)) \/ (exists p, In p xs /\ exists s', EV (snd p) => s')) as [|].
    { apply list_dec. intros (?&?) ?. cbn.
      assert (exists A, In (n, A) As) as (A&?). apply H1; eauto.
      eauto. }
    + left. constructor. intros. specialize (H4 (i, s)). eauto.
    + destruct H4 as ((l&s)&?&(s'&?)).
      right. exists (rectm (update xs l s')). econstructor; eauto.

  - right. edestruct IHhas_ty as [? | [? ?]]; eauto.
    + edestruct (can_form_rectm H H1) as [? [? ?]]; try reflexivity. subst.
      rename x into xs.
      enough (exists x, In (j, x) xs) as (?&?).
      * eexists. constructor. eauto.
      * inversion H; eauto.
    + eexists. constructor. eassumption.
  - edestruct (IHhas_ty1 pat_ty_subst pat_progress s0 A0) as [|[? ?]]; eauto.
    + right. edestruct (pat_progress _ _ _ _ _ H H0). eexists. econstructor. eauto.
    + right. eexists. apply E_LetL; eauto.
Qed.

(** Preservation *)

(* Lemma scons_p_head2' {X} {m n} (f : fin m -> X) (g : fin n -> X): *)
(*   pointwise_relation _ eq (zero_p m >> (scons_p m f g)) f. *)
(* Proof. *)
(*   intros z. *)
(*   unfold funcomp. *)
(*  induction m. *)
(*   - inversion z. *)
(*   - destruct z. *)
(*     + simpl. simpl. now rewrite IHm. *)
(*     + reflexivity. *)
(* Qed. *)

(* Lemma scons_p_tail2' X  m n (f : fin m -> X) (g : fin n -> X) : *)
(*   pointwise_relation _ eq (shift_p m >> scons_p m f g) g. *)
(* Proof. intros z; unfold funcomp. induction m; cbn; eauto. Qed. *)

(* Lemma scons_p_comp2' X Y m n (f : fin m -> X) (g : fin n -> X) (h : X -> Y): *)
(*   pointwise_relation _ eq ((scons_p m f g) >> h) (scons_p m (f >> h) (g >> h)). *)
(* Proof. *)
(*   intros x. *)
(*   unfold funcomp. *)
(*   destruct (destruct_fin x) as [[x' ->]|[x' ->]]. *)
(*   - (* TODO this might be one of the problems Yannick encountered. *)
(*      * *) *)
(*     now setoid_rewrite scons_p_head'. *)
(*   - now setoid_rewrite scons_p_tail'. *)
(* Qed. *)

(* Instance funcomp_morphism {X Y Z} : *)
(*   Proper (@pointwise_relation Y Z eq ==> @pointwise_relation X Y eq ==> @pointwise_relation X Z eq) funcomp. *)
(* Proof. *)
(*   cbv - [funcomp]. *)
(*   intros g0 g1 Hg f0 f1 Hf x. *)
(*   unfold funcomp. rewrite Hf, Hg. *)
(*   reflexivity. *)
(* Qed. *)

(* Lemma forall_pointwise {X} {Y: X} (f g: X -> Y) : (forall x, f x = g x) -> pointwise_relation _ eq f g. *)
(* Proof. *)
(*   intros * H x. apply H. *)
(* Qed. *)

(* Lemma crl0: *)
(*   forall (m n p : nat) (pt : pat m) (s : tm m n) (t : tm m (p + n)) (A B : ty m) (m' n' : nat) *)
(*     (Delta: ctx m) (Gamma: dctx n m) *)
(*     (Delta0 : ctx m') (Gamma0 : dctx n' m') (xi : fin m -> fin m') (zeta : fin n -> fin n') *)
(*     (Gamma': fin p -> ty m) (H: pat_ty m p pt A Gamma') *)
(*     (ty1: TY Delta;Gamma |- s : A) (ty2: TY Delta;scons_p p Gamma' Gamma |- t : B) *)
(*   (IHty1 : forall (m' n' : nat) (Delta0 : ctx m') (Gamma0 : dctx n' m') (xi : fin m -> fin m') *)
(*             (zeta : fin n -> fin n'), *)
(*           (forall x : fin m, (Delta x) ⟨xi⟩ = Delta0 (xi x)) -> *)
(*           (forall x : fin n, (Gamma x) ⟨xi⟩ = Gamma0 (zeta x)) -> TY Delta0;Gamma0 |- s ⟨xi;zeta⟩ : A ⟨xi⟩) *)
(*   (IHty2 : forall (m' n' : nat) (Delta0 : ctx m') (Gamma0 : dctx n' m') (xi : fin m -> fin m') *)
(*             (zeta : fin (p + n) -> fin n'), *)
(*           (forall x : fin m, (Delta x) ⟨xi⟩ = Delta0 (xi x)) -> *)
(*           (forall x : fin (p + n), (scons_p p Gamma' Gamma x) ⟨xi⟩ = Gamma0 (zeta x)) -> *)
(*           TY Delta0;Gamma0 |- t ⟨xi;zeta⟩ : B ⟨xi⟩) *)
(*   (H0: forall x : fin m, (Delta x) ⟨xi⟩ = Delta0 (xi x)) (H': forall x : fin n, (Gamma x) ⟨xi⟩ = Gamma0 (zeta x)), *)

(*  TY Delta0;Gamma0 |- letpat p pt ⟨xi⟩ s ⟨xi;zeta⟩ t ⟨xi;upRen_p p zeta⟩ : B ⟨xi⟩. *)
(* Proof. *)
(*   intros m n p pt s t A B m' n' Delta Gamma Delta0 Gamma0 xi zeta Gamma' H ty1 ty2 IHty1 IHty2 H0 H'. *)
(*   cbn. asimpl. apply letpat_ty  with (A0 := A⟨xi⟩) (Gamma'0 := Gamma' >> ⟨xi⟩); eauto. *)
(*   + unfold funcomp. *)
(*     (* TODO the unfold funcomp should not be necessary anymore when I use Yannicks appraoch *) *)
(*     substify. *)
(*     eauto. *)
(*   + asimpl. *)
(*     (* Hint Opaque scons_p : rewrite. *) *)
(*     (* Hint Opaque subst_ty : rewrite. *) *)
(*     eapply IHty2. eauto. *)
(*     * *)
(*       (** * works *) *)
(*       (* DONE try to make the goal into pointwise_relation *) *)
(*       (* enough (H2: pointwise_relation _ eq ((scons_p p Gamma' Gamma ) >> (ren_ty xi)) ((upRen_p p zeta ) >> (scons_p p (Gamma' >> ren_ty xi) Gamma0 ))) by apply H2. *) *)
(*       (* intros z. *) *)
(*       (* adrian: had to add the following line to make it compile.*) *)
(*       (* unfold dctx in Gamma, Gamma0. unfold upRen_p. *) *)
(*       (* (* TODO setoid-asimpl does not work with scons_p yet *) *) *)
(*       (* (* DONE use normal rewrite for asimpl_fext *) *) *)
(*       (* (*  * works the same as it should (because it only used rewrite to begin with) *) *) *)
(*       (* (* match goal with *) *) *)
(*       (* (*    |[|- _ =  ?h (?f ?s)] => change (h (f s)) with ((f >> h) s); idtac "fsimpl12" *) *) *)
(*       (* (*    |[|-  ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s); idtac "fsimpl13" *) *) *)
(*       (* (* end. *) *) *)
(*       (* (* match goal with *) *) *)
(*       (* (*    |[|- _ =  ?h (?f ?s)] => change (h (f s)) with ((f >> h) s); idtac "fsimpl12" *) *) *)
(*       (* (*    |[|-  ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s); idtac "fsimpl13" *) *) *)
(*       (* (* end. *) *) *)
(*       (* (* autorewrite with FunctorInstances. *) *) *)

(*       (* setoid_rewrite scons_p_comp2'. *) *)
(*       (* setoid_rewrite scons_p_head2'. *) *)
(*       (* match goal with *) *)
(*       (*    | [|- context[(?f >> ?g) >> ?h]] => *) *)
(*       (*      change ((f >> g) >> h) with (f >> (g >> h)) (* AsimplComp *); idtac "fsimpl3" *) *)
(*       (* end. *) *)
(*       (* setoid_rewrite scons_p_tail2'. *) *)

(*       (* (* TODO can we do it without unfolding funcomp? *) *) *)
(*       (* unfold funcomp. *) *)
(*       (* setoid_rewrite H'. *) *)

(*       intros z. *)
(*       unfold dctx in Gamma, Gamma0. unfold upRen_p. *)
(*       fsimpl. *)
(*       unfold funcomp. *)
(*       Hint Transparent scons_p : rewrite. *)
(*       Set Typeclasses Debug. *)
(*       try rewrite_strat innermost H'. *)

(*       (* TODO somehow the approach of wrapping it in id or AW does nto work with scons_p_comp here *) *)
(* (*        * but a rewrite strat does help *) *)
(* (*        * but the rewrite_strat with subterms works well *) *)
(*       (* rewrite_strat scons_p_comp'. *) *)
(*       (* rewrite_strat subterms scons_p_comp'. *) *)
(*       (* setoid_rewrite scons_p_head'. *) *)
(*       (* setoid_rewrite scons_p_tail'. *) *)
(*       (* setoid_rewrite H'. *) *)
(*       (* reflexivity. *) *)

(*       (* TODO this rewrites too eagerly and also uses the eq that is applied to the scons_p *) *)
(* (*        * If I don't unfold funcomp this would not be a problem *) *)
(* (*        * But I'm wondering why this happens here but not in the other file with just scons?*) *)
(*       (* rewrite scons_p_comp'. *) *)
(*       (* Set Printing All. *) *)
(*       (* Fail setoid_rewrite scons_p_comp'. *) *)
(*       (* TODO koennte bei problemen mit rewriting helfen *) *)
(*       (* Set Keyed Unification. *) *)
(*       (* autorewrite with FunctorInstances2. *) *)
(*       (* Unset Printing Notations. *) *)
(*   (*     Set Typeclasses Debug. *) *)
(*   (*     setoid_rewrite scons_p_comp'. *) *)
(*   (*     setoid_rewrite (scons_p_comp' _ _ (ren_ty xi)). *) *)
(*   (*     setoid_rewrite (scons_p_comp' _ _ (scons_p p (fun x : fin p => ren_ty xi (Gamma' x)) Gamma0)). *) *)
(*   (*     unfold funcomp. *) *)
(*   (*     setoid_rewrite scons_p_head'. *) *)
(*   (*     (* match goal with *) *) *)
(*   (*     (*    | [|- context[(?f >> ?g) >> ?h]] => *) *) *)
(*   (*     (*      change ((f >> g) >> h) with (f >> (g >> h)) (* AsimplComp *); idtac "fsimpl3" *) *) *)
(*   (*     (* end. *) *) *)
(*   (*     setoid_rewrite scons_p_tail'. *) *)
(*   (*     (* autorewrite with FunctorInstances. *) *) *)
(*   (*     (* fsimpl_fext. *) *) *)
(*   (*     (* asimpl_fext. *) *) *)
(*   (* (* scons_p p (Gamma' >> ⟨xi⟩) (Gamma >> ⟨xi⟩) z = scons_p p (Gamma' >> ⟨xi⟩) (zeta >> Gamma0) z *) *) *)
(*   (*     (* asimpl. *) *) *)
(*   (*     (* unfold funcomp. *) *) *)
(*   (*     (* setoid_rewrite scons_p_comp'. *) *) *)
(*   (*     unfold funcomp. *) *)
(*   (*     (* DONE why does it not use the morphism? *) *) *)
(* (*   (*      * because my scons_p morphism had (pointwise_relation) in the conclusion (because scons_p returns a function) *) *) *)
(* (*   (*      * but here we want to solve an equality so we need eq in the conclusion. *) *) *)
(* (*   (*      * therefore we need to inline the extensional equality in the morphism's signature by taking another eq argument and returning an eq of the results *) *) *)
(*   (*     setoid_rewrite H'. *) *)
(*   (*     reflexivity. *) *)
(* Qed. *)

Lemma context_renaming_lemma m m' n n' (Delta: ctx m') (Gamma: dctx n' m')                                                   (s: tm m n) A (xi : fin m -> fin m') (zeta: fin n -> fin n') Delta' (Gamma' : dctx n m):
  (forall x, (Delta' x)⟨xi⟩ = Delta (xi x)) ->
  (forall (x: fin n) , (Gamma' x)⟨xi⟩ =  (Gamma (zeta x))) ->
  TY Delta'; Gamma' |- s : A -> TY Delta; Gamma |- s⟨xi;zeta⟩ : A⟨xi⟩.
Proof.
  intros H H' ty. autorevert ty.
  depind ty; asimpl; intros; subst; try now (econstructor; eauto).
  - rewrite H0. constructor.
  - constructor. eapply IHty; eauto.
    auto_case; asimpl.
  - cbn. econstructor. apply IHty; eauto.
    + auto_case; try now asimpl. rewrite <- H. now asimpl.
    + intros. asimpl. rewrite <- H'. now asimpl.
  - cbn. eapply T_Tapp with (A0 := A⟨xi⟩) (B0 := ren_ty (upRen_ty_ty xi) B).
    asimpl in IHty. eapply IHty; eauto.
    eapply sub_weak; eauto. now asimpl.
  - econstructor; eauto.
    + intros.
      eapply in_map_iff in H5. destruct H5 as ([]&?&?). inv H5.
      eapply in_map_iff in H6. destruct H6 as ([j A']&?&?). inv H5.
      eapply H3; eassumption.
  - cbn. econstructor; eauto. now apply in_map.
  - cbn. asimpl. apply letpat_ty  with (A0 := A⟨xi⟩) (Gamma'0 := Gamma' >> ⟨xi⟩); eauto.
    + unfold funcomp.
      (* TODO the unfold funcomp should not be necessary anymore when I use Yannicks appraoch *)
      substify.
      eauto.
    + asimpl.
      (* Hint Opaque scons_p : rewrite. *)
      (* Hint Opaque subst_ty : rewrite. *)
      eapply IHty2. eauto.
      * intros z.
        unfold dctx in Gamma, Gamma0. unfold upRen_p.
        asimpl.
        unfold funcomp.
        now setoid_rewrite H'.
  - econstructor. eauto. eapply sub_weak; eauto.
Qed.

Lemma context_renaming_lemma' m m' n n' (Delta: ctx m') (Gamma: dctx n' m')                                                   (s: tm m n) A (xi : fin m -> fin m') (zeta: fin n -> fin n') Delta' (Gamma' : dctx n m):
  (forall x, (Delta' x)⟨xi⟩ = Delta (xi x)) ->
  (forall (x: fin n) , (Gamma' x)⟨xi⟩ =  (Gamma (zeta x))) ->
  TY Delta'; Gamma' |- s : A -> forall s' A', s' = s⟨xi;zeta⟩ -> A' = A⟨xi⟩ -> TY Delta; Gamma |- s' : A'.
Proof. intros. subst. now eapply context_renaming_lemma. Qed.

Lemma context_morphism_lemma m m' n n' (Delta: ctx m) (Delta': ctx m') (Gamma: dctx n m) (s: tm m n) A (sigma : fin m -> ty m') (tau: fin n -> tm m' n') (Gamma' : dctx n' m'):
  (forall x, SUB Delta' |- sigma x <: (Delta x)[sigma]) ->
  (forall (x: fin n) ,  TY Delta'; Gamma' |- tau x : subst_ty sigma (Gamma x)) ->
  TY Delta; Gamma |- s : A -> TY Delta'; Gamma' |- s[sigma;tau] : A[sigma].
Proof.
   intros eq1 eq2 ty. autorevert ty.
   depind ty; intros; subst; asimpl; try now (econstructor; eauto).
  - constructor. eapply IHty; eauto.
    auto_case; asimpl.
    +  assert (subst_ty sigma (Gamma f)  = ((Gamma f)[sigma]⟨id⟩)) as -> by (now asimpl) .
       eapply context_renaming_lemma; eauto; now asimpl.
    + econstructor.
  - constructor. eapply IHty; eauto.
    + auto_case.
      * asimpl.
        specialize (eq1 f).
        eapply sub_weak1 with (C := A[sigma]) in eq1; eauto.  asimpl in eq1. eapply eq1.
    + intros x. asimpl.
      assert ((Gamma x) [sigma >> ⟨↑⟩] = (Gamma x)[sigma]⟨↑⟩) by (now asimpl).
      auto_unfold in *. rewrite H.
      eapply context_renaming_lemma; try eapply eq2.
      * intros. now asimpl.
      * intros. now asimpl.
  - eapply T_Tapp with (A0 := subst_ty sigma A) (B0 := subst_ty (up_ty_ty sigma) B).
    asimpl in IHty. eapply IHty; eauto.
    eapply sub_substitution; eauto.
    now asimpl.
  - econstructor; eauto.
    + intros.
      eapply in_map_iff in H5. destruct H5 as ([]&?&?). inv H5.
      eapply in_map_iff in H4. destruct H4 as ([j A']&?&?). inv H4.
      eapply H3; eauto.
  - econstructor; eauto. now apply in_map.
  - econstructor; eauto.
     { eapply IHty2.
      * eauto.
      * intros x.
        destruct (destruct_fin x) as [[x' ->] |[x' ->]]; asimpl; eauto.
        -- eapply T_Var'. now asimpl.
        -- eapply context_renaming_lemma'; try eapply eq2.
           (* TODO try out why exactly only the scons_p_* lemmas have issues with evars *)
           Unshelve.
           5: exact id.
           5: exact (shift_p p).
           5: exact x'.
           all: now asimpl.
           (* try now asimpl. *)
           (* intros z. *)
           (* now asimpl. *)
           (* (* TODO setoid-asimpl does not work with scons_p yet *) *)
           (* intros x. *)
           (* now asimpl. *)
           (* (* now asimpl_fext. *) *)
     }
  - econstructor.
    + eapply IHty; eauto.
    + eapply sub_substitution; eauto.
Qed.

Lemma ty_inv_abs m n Delta Gamma A A' B C (s: tm m (S n)):
  TY Delta;Gamma |- abs A s : C   ->   SUB Delta |- C <: arr A' B   ->
  (SUB Delta |- A' <: A /\
    exists B', TY Delta; A .: Gamma |- s : B' /\ SUB Delta |- B' <: B).
Proof.
  intros H. depind H; intros.
   - inv H0. split; eauto.
   - edestruct (IHhas_ty pat_ty_subst pat_progress  _ _ _ _ (eq_refl _) (sub_trans _ _ _ _ _ H0 H1)) as (?&?&?&?).
     split.
     + assumption.
     + eauto.
Qed.

Lemma ty_inv_rec {m n} {Delta Gamma A As'} xs  :
  TY Delta;Gamma |- rectm xs: A  ->  SUB Delta |- A <: recty As' ->
   (  (forall (i : nat) (s : tm m n) B',
          In (i, s) xs -> In (i, B') As' ->  exists (B : ty m),  TY Delta;Gamma |- s : B /\ SUB Delta |- B <: B')).
Proof.
  intros H. depind H; intros.
  - inv H4. eauto.
    assert (exists A, In (i, A) As) as [A ?].
    + apply H1. eauto.
    + specialize (H2 _ _ _ H5 H4).
      destruct (H9 _ _ H6) as (?&?&?).
      assert (x = A) as -> by eauto using unique_spec.
      eauto.
  - eauto using sub_trans.
Qed.

Lemma ty_subst m n (Gamma: dctx m n) (Delta: ctx n) Delta' s A:
    (forall x, SUB Delta' |- Delta' x <: Delta x) ->
  TY Delta; Gamma |- s : A -> TY Delta'; Gamma |- s : A.
Proof.
  intros eq H. autorevert H. depind H; eauto; intros; try now (econstructor; eauto).
  - econstructor; eauto. asimpl. eapply IHhas_ty. auto_case; eauto using sub_refl.
    eapply sub_weak; try reflexivity. apply eq. intros x. now asimpl.
  - econstructor; eauto.
    replace A with (A[ids]) by (now asimpl). replace A' with (A'[ids]) by (now asimpl).
    eapply sub_substitution; eauto. intros x.
    asimpl. econstructor. eauto.
 - econstructor; eauto. eapply sub_substitution with (sigma := ids) (Delta':=Delta') in H0; eauto.
    asimpl in H0. eapply H0. intros x. econstructor. asimpl. eapply eq.
Qed.

Lemma ty_inv_tabs {m n} {Delta Gamma A A' B C} (s : tm (S m) n):
  TY Delta;Gamma |- tabs A s : C -> SUB Delta |- C <: all A' B   ->
  (SUB Delta |- A' <: A /\ exists B',
   TY (A'.:Delta) >> ren_ty ↑; Gamma >> ren_ty ↑ |- s : B' /\ SUB (A' .: Delta) >> ren_ty ↑ |- B' <: B).
Proof.
  intros H. depind H; intros.
  - inv H0. split; eauto.
    eexists. split; eauto.
    eapply ty_subst; try eapply H.
    auto_case. eapply sub_weak; try reflexivity; eauto.
  - eauto using sub_trans.
Qed.

Variable pat_ty_eval : forall m n p pt s A (Gamma: fin n -> ty m) Gamma' Delta sigma, pat_ty m p pt A Gamma' -> TY Delta; Gamma |- s : A -> pat_eval m n p pt s sigma -> forall (x: fin p), TY Delta; Gamma |- sigma x : Gamma' x.

Theorem preservation m n Delta Gamma (s: tm m n) t A :
  TY Delta;Gamma |- s : A -> EV s => t ->
  TY Delta;Gamma |- t : A.
Proof.
  intros H_ty H_ev. autorevert H_ev.
  induction H_ev; intros; eauto using ty.
  all: try now (depind H_ty; [econstructor; eauto|eapply T_Sub; eauto]).
  - depind H_ty; [|eauto].
    + inv H_ty1; subst.
      * replace B with (B[ids]) by (now asimpl).
        eapply context_morphism_lemma; eauto.
        -- intros. asimpl. repeat constructor. now apply sub_refl.
        -- intros [|]; intros; cbn; asimpl;  eauto. econstructor; eauto.
      * pose proof (ty_inv_abs _ _ _ _ _ _ _ _ _ H H0) as (?&?&?&?).
        eapply T_Sub; eauto.
        replace x with (x[var_ty]) by (now asimpl).
        eapply context_morphism_lemma; eauto.
        -- intros. asimpl. repeat constructor. apply sub_refl.
        -- intros [|]; intros; cbn; asimpl; eauto; econstructor; eauto.
     + asimpl. econstructor; eauto.
  - depind H_ty; eauto.
    + depind H_ty.
      * asimpl in H_ty.
        eapply context_morphism_lemma; try eapply H_ty; eauto.
        -- auto_case; asimpl; eauto using sub_refl.
        -- intros x. asimpl. constructor.
      * pose proof (ty_inv_tabs _ H_ty H) as (?&?&?&?).
        eapply T_Sub.
        eapply context_morphism_lemma; eauto.
        -- auto_case; asimpl; eauto.
        -- intros z. asimpl. constructor.
        -- eapply sub_substitution; eauto.
           auto_case; asimpl.
    + econstructor; eauto.
  -  depind H_ty; eauto.
    + depind H_ty.
      * eapply H2; eauto.
      * pose proof (ty_inv_rec _ H_ty H  _ _ _ H1 H0) as(?&?&?).
        subst. eapply T_Sub; eauto.
    + econstructor; eauto.
  - depind H_ty.
    + replace B with (B[ids]) by now asimpl.
      eapply context_morphism_lemma; try now apply H_ty2.
      * intros. asimpl. constructor. now apply sub_refl.
      * intros. destruct (destruct_fin x) as [[]|[]]; subst.
        (* TODO why did I have to do `exact Gamma'` here twice? *)
        -- asimpl. eapply pat_ty_eval; eauto. (* exact Gamma'. *)
        -- asimpl. constructor. (* exact Gamma'. *)
    + eapply T_Sub; eauto.
  - depind H_ty; [|eapply T_Sub; eauto].
    econstructor; eauto.
    + intros.
      apply update_char in H5 as [|(->&->)]; eauto.
Qed.

End Pattern.

(* TODO prove morphisms with Marcel's project. Also why does the UIP axiom appear here? *)
Print Assumptions preservation.

author: addap

repo: autosubst-ocaml

save_path: github-repos/coq/addap-autosubst-ocaml


text:
(******************************************************************************)
(* PipeCheck: Specifying and Verifying Microarchitectural                     *)
(* Enforcement of Memory Consistency Models                                   *)
(*                                                                            *)
(* Copyright (c) 2014 Daniel Lustig, Princeton University                     *)
(* All rights reserved.                                                       *)
(*                                                                            *)
(* This library is free software; you can redistribute it and/or              *)
(* modify it under the terms of the GNU Lesser General Public                 *)
(* License as published by the Free Software Foundation; either               *)
(* version 2.1 of the License, or (at your option) any later version.         *)
(*                                                                            *)
(* This library is distributed in the hope that it will be useful,            *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of             *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU          *)
(* Lesser General Public License for more details.                            *)
(*                                                                            *)
(* You should have received a copy of the GNU Lesser General Public           *)
(* License along with this library; if not, write to the Free Software        *)
(* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  *)
(* USA                                                                        *)
(******************************************************************************)

Require Import Arith.
Require Import List.
Import ListNotations.
Require Import Ascii.
Require Import String.
Require Import util2.
Require Import risc.
Require Import ppo.
Require Import litmus.

Definition AllPPOGraphs := GraphsToVerifyTSOPPO (RISC_Pipeline 1).

Definition AllLitmusTestGraphs :=
    map (fun t => t (RISC_Pipeline 4)) AllLitmusTests.

Definition AllGraphs :=
  AllPPOGraphs ++
  fold_left (app (A:=_))
    (AllLitmusTestGraphs)
    [].

Extraction Language Ocaml.
Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inductive list => "list" [ "[]" "(::)" ].
Extract Inductive nat => int [ "0" "(fun x -> x + 1)" ]
  "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
Extract Inductive ascii => char
[
"(* If this appears, you're using Ascii internals. Please don't *) (fun (b0,b1,b2,b3,b4,b5,b6,b7) -> let f b i = if b then 1 lsl i else 0 in Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))"
]
"(* If this appears, you're using Ascii internals. Please don't *) (fun f c -> let n = Char.code c in let h i = (n land (1 lsl i)) <> 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))".

Extract Constant plus => "( + )".
Extract Constant mult => "( * )".
Extract Constant beq_nat => "( = )".

(*
Extract Constant zero => "'λ000'".
Extract Constant one => "'λ001'".
Extract Constant shift =>
 "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)".
Extract Inlined Constant ascii_dec => "(=)".
*)
Extraction "riscgraphs.ml" AllGraphs.

author: daniellustig

repo: pipecheck

save_path: github-repos/coq/daniellustig-pipecheck


text:
Require Export TrInccount.
Require Export TrInckn.
Require Export TrIncacc_exec.
Require Export TrIncacc_new.
Require Export TrIncvreq_mon.

Section TrIncprops1.

  Local Open Scope eo.
  Local Open Scope proc.

  Context { dtc                 : DTimeContext        }.
  Context { minbft_context      : MinBFT_context      }.
  Context { m_initial_keys      : MinBFT_initial_keys }.
  Context { u_initial_keys      : USIG_initial_keys   }.
  Context { usig_hash           : USIG_hash           }.
  Context { minbft_auth         : MinBFT_auth         }.

  Lemma accepted_counter_if_know_UI_primary :
    forall {eo    : EventOrdering}
           (e     : Event)
           (R     : Rep)
           (r     : Request)
           (i     : nat)
           (l     : list name),
      In (send_accept (accept r i) l) (M_output_ls_on_event (MinBFTlocalSys R) e)
      ->
      exists (s  : MAIN_state)
             (s1 : TRINC_state)
             (s2 : LOG_state)
             (ui : UI),
        M_run_ls_on_event (MinBFTlocalSys R) e = Some (MinBFTlocalSys_new R s s1 s2)
        /\ kc_knows (minbft_data_rdata (request_data (current_view s) r ui)) s2
        /\ kc_Tknows ui s2
        /\ kc_trust2owner ui = Some (MinBFTprimary (current_view s))
        /\ ui2cid ui = 0
        /\ ui2counter ui = i.
  Proof.
    introv h.
    apply accepted_counter_if_received_UI_primary in h.
    exrepnd.
    exists s s1 s2 ui.
    simpl.
    dands; auto; unfold MinBFT_data_knows; simpl; subst; allrw; eauto 3 with minbft;[].
    unfold request_data_in_log; simpl.
    allrw <-; autorewrite with minbft; allrw; auto.
  Qed.

  Lemma kc_Tknows_implies :
    forall  (ui : UI) (l : LOG_state),
      kc_Tknows ui l
      -> exists en,
        In en l                     (* FIX: Do we need this one instead? find_entry rd l = Some e *)
        /\ ui_in_log ui l = true    (* FIX: do we need this one? *)
        /\
        (
          (exists rd, request_data2ui rd = ui )
          \/
          (In ui (log_entry_commits en))
        ).
  Proof.
    introv H.
    unfold kc_Tknows in *.
    unfold kc_knows in *. simpl in *.
    unfold MinBFT_data_knows in *.
    unfold MinBFT_data_in_log in *.

    unfold ui_in_log in *.
    eapply existsb_exists in H.
    exrepnd.
    rename x into en.

    unfold ui_in_log_entry in *.
    dest_cases w;[|].
    {
      exists en; dands; eauto.
      eapply existsb_exists.
      exists en. dands; eauto.
      dest_cases x.
    }
    {
      dest_cases x;[].
      exists en; dands; eauto.
      eapply existsb_exists.
      exists en; dands; eauto.
      dest_cases x;[].
      dest_cases y.
    }
  Qed.

(*  Lemma uis_where_verified :
    forall {eo : EventOrdering} (e : Event) (l : LOG_state) (u : USIG_state) (ui : UI),
      is_replica e
      -> M_state_sys_on_event MinBFTsys e LOGname = Some l
      -> M_state_sys_on_event MinBFTsys e USIGname = Some u
      -> kc_Tknows ui l
      ->
      exists hd,
        kc_knows (minbft_data_hdata hd) l
        /\ verify_hash_usig hd (ui2digest ui) (usig_local_keys u) = true.
  Proof.
    introv isr eqst1 eqst2 unl.

    unfold kc_Tknows in unl; simpl in unl.
    unfold MinBFT_data_knows in unl; simpl in unl.

    rewrite M_state_sys_on_event_unfold in eqst1.
    rewrite M_state_sys_on_event_unfold in eqst2.

    apply map_option_Some in eqst1.
    apply map_option_Some in eqst2.
    exrepnd; try rev_Some.

    rewrite eqst1 in eqst2; ginv.

    unfold is_replica in *; exrepnd.

    revert dependent u.
    revert dependent l.
    revert dependent a.
    rewrite isr0; simpl.

    (* WARNING *)
    clear isr0.

    induction e as [e ind] using predHappenedBeforeInd;[]; introv run stl inlog stu.

    rewrite M_run_ls_on_event_unroll in run.
    rewrite M_run_ls_before_event_unroll_on in run.

    destruct (dec_isFirst e) as [d|d].

    {
      clear ind.

      unfold M_run_ls_on_this_one_event in run; simpl in *.
      apply map_option_Some in run; exrepnd; rev_Some.
      unfold M_break in run0; simpl in *; smash_minbft; repnd; simpl in *.
      apply option_map_Some in run0; exrepnd; subst; simpl in *.

      minbft_dest_msg Case a0; simpl in *;
        try (complete (inversion Heqx; subst; simpl in *;
                       unfold state_of_subcomponents in *;
                       simpl in *; ginv));
        [| |].

      { Case "Request".

        unfold call_create_ui, bind in *; simpl in *.
        inversion Heqx; subst; simpl in *; clear Heqx;
          unfold state_of_subcomponents in *; simpl in *; ginv.
        unfold ui_in_log in *; simpl in *.
        unfold ui_in_log_entry in *; simpl in *.
        smash_minbft; simpl in *.
        unfold MinBFT_data_knows; simpl.
        unfold hash_data_in_log_entry, RequestData2HashData; simpl.
        exists (Build_HashData initial_view (request_b m) (Build_preUI r 1)).
        simpl; smash_minbft; GC; dands; auto. }

      { Case "Prepare".

        unfold call_verify_ui, bind in *; simpl in *; smash_minbft;
          try (complete (unfold state_of_subcomponents in *; simpl in *;
                         ginv; eapply ind in run1; eauto; eauto 3 with eo)).

        { unfold state_of_subcomponents in *; simpl in *; ginv.
          unfold ui2rep, ui_in_log in *; simpl in *; autorewrite with bool in *; subst.
          unfold ui_in_log_entry in *; simpl in *; autorewrite with minbft in *; smash_minbft.
          unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
          exists (prepare2hash_data p); dands; auto.
          unfold MinBFT_data_knows; simpl.
          unfold hash_data_in_log_entry; simpl; smash_minbft. }

        { unfold state_of_subcomponents in *; simpl in *; ginv.
          unfold ui2rep, ui_in_log in *; simpl in *; autorewrite with bool in *; subst.
          unfold ui_in_log_entry in *; simpl in *; autorewrite with minbft in *; smash_minbft.

          { unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
            exists (prepare2hash_data p); dands; auto.
            unfold MinBFT_data_knows; simpl.
            unfold hash_data_in_log_entry; simpl; smash_minbft. }

          { exists (Build_HashData
                      (prepare2view p)
                      (request_b (prepare2request p))
                      (Build_preUI r 1)); simpl.
            autorewrite with minbft; dands; auto.
            unfold MinBFT_data_knows; simpl.
            unfold hash_data_in_log_entry; simpl; smash_minbft. } }

        { unfold state_of_subcomponents in *; simpl in *; ginv.
          unfold ui2rep, ui_in_log in *; simpl in *; autorewrite with bool in *; subst.
          unfold ui_in_log_entry in *; simpl in *; autorewrite with minbft in *; smash_minbft.

          { unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
            exists (prepare2hash_data p); dands; auto.
            unfold MinBFT_data_knows; simpl.
            unfold hash_data_in_log_entry; simpl; smash_minbft. }

          { unfold invalid_prepare in *; smash_minbft.
            apply valid_prepare_implies_view in Heqx0; rewrite Heqx0 in *.
            autorewrite with minbft in *; tcsp. } }
      }

      { Case "Commit".
        unfold call_verify_ui, bind in *; simpl in *; smash_minbft;
          try (complete (unfold state_of_subcomponents in *; simpl in *; ginv));[].

        unfold call_prepare_already_in_log, bind_pair, bind in *; simpl in *; smash_minbft;[].
        unfold call_log_commit, bind in *; simpl in *; smash_minbft;[|].

        { unfold invalid_commit, valid_commit in *; smash_minbft. }

        { unfold call_is_committed, bind in *; simpl in *; smash_minbft;[|].

          { unfold state_of_subcomponents in *; simpl in *; ginv; simpl in *.
            smash_minbft; repndors; ginv.
            unfold ui_in_log_entry in *; simpl in *; autorewrite with minbft in *; smash_minbft;[|].

            { exists (commit2hash_data_i c).
              unfold verify_UI in *; autorewrite with minbft in *; dands; auto.
              unfold MinBFT_data_knows; simpl.
              unfold hash_data_in_log_entry; simpl; smash_minbft. }

            { unfold add_commit2commits, ui2rep in *; simpl in *; smash_minbft;
                repndors; subst; tcsp;[| |].
              { exists (Build_HashData
                          (commit2view c)
                          (request_b (commit2request c))
                          (Build_preUI (commit2sender_j c) 1)); simpl.
                autorewrite with minbft; dands; auto.
                unfold MinBFT_data_knows; simpl.
                unfold hash_data_in_log_entry; simpl; smash_minbft; tcsp. }
              { exists (commit2hash_data_j c).
                unfold verify_UI in *; autorewrite with minbft in *; dands; auto.
                unfold MinBFT_data_knows; simpl.
                unfold hash_data_in_log_entry; simpl; smash_minbft. }
              { unfold ui2digest; simpl.
                exists (Build_HashData
                          (commit2view c)
                          (request_b (commit2request c))
                          (Build_preUI r 1)); simpl.
                autorewrite with minbft; dands; auto;[].
                unfold MinBFT_data_knows; simpl.
                unfold hash_data_in_log_entry; simpl; smash_minbft; tcsp. }
            }
          }

          { unfold state_of_subcomponents in *; simpl in *; ginv.
            unfold ui_in_log in *; simpl in *; autorewrite with bool in *.
            unfold ui_in_log_entry in *; simpl in *; smash_minbft;[|].

            { exists (commit2hash_data_i c).
              unfold verify_UI in *; autorewrite with minbft in *; dands; auto.
              unfold MinBFT_data_knows; simpl.
              unfold hash_data_in_log_entry; simpl; smash_minbft. }

            { unfold add_commit2commits, ui2rep in *; simpl in *; smash_minbft;
                repndors; subst; tcsp;[| |].
              { exists (Build_HashData
                          (commit2view c)
                          (request_b (commit2request c))
                          (Build_preUI (commit2sender_j c) 1)); simpl.
                autorewrite with minbft; dands; auto.
                unfold MinBFT_data_knows; simpl.
                unfold hash_data_in_log_entry; simpl; smash_minbft; tcsp. }
              { exists (commit2hash_data_j c).
                unfold verify_UI in *; autorewrite with minbft in *; dands; auto.
                unfold MinBFT_data_knows; simpl.
                unfold hash_data_in_log_entry; simpl; smash_minbft. }
              { unfold ui2digest; simpl.
                exists (Build_HashData
                          (commit2view c)
                          (request_b (commit2request c))
                          (Build_preUI r 1)); simpl.
                autorewrite with minbft; dands; auto;[].
                unfold MinBFT_data_knows; simpl.
                unfold hash_data_in_log_entry; simpl; smash_minbft; tcsp. }
            }
          }
        }
      }
    }

    {
      apply map_option_Some in run; exrepnd; rev_Some.
      applydup M_run_ls_on_event_ls_is_minbft in run1; exrepnd; subst.

      unfold M_run_ls_on_this_one_event in run0; simpl in *.
      apply map_option_Some in run0; exrepnd; rev_Some.
      unfold M_break in run2; simpl in *; smash_minbft; repnd; simpl in *.
      apply option_map_Some in run2; exrepnd; subst; simpl in *.

      minbft_dest_msg Case a0; simpl in *;
        try (complete (inversion Heqx; subst; simpl in *;
                       unfold state_of_subcomponents in *;
                       simpl in *; ginv;
                       eapply ind in run1; eauto; eauto 3 with eo));
        [| |].

      { Case "Request".

        unfold call_create_ui, bind in *; simpl in *.
        inversion Heqx; subst; simpl in *; clear Heqx;
          unfold state_of_subcomponents in *; simpl in *; ginv.

        rewrite ui_in_log_log_new_prepare in inlog; simpl in *.
        smash_minbft; simpl in *.

        { unfold MinBFT_data_knows; simpl.
          exists (Build_HashData
                    (current_view s)
                    (request_b m)
                    (Build_preUI (usig_id s1) (S (usig_counter s1)))).
          rewrite hash_data_in_log_log_new_prepare.
          Opaque HashData_Deq.
          simpl.
          unfold RequestData2HashData; simpl.
          smash_minbft. }

        eapply ind in run1; try exact inlog; try reflexivity; eauto 3 with eo;[].
        exrepnd.
        exists hd.

        unfold MinBFT_data_knows; simpl.
        rewrite hash_data_in_log_log_new_prepare; simpl in *.
        unfold RequestData2HashData; simpl; allrw.
        smash_minbft. }

      { Case "Prepare".

        unfold call_verify_ui, bind in Heqx; simpl in *; smash_minbft;
          try (complete (unfold state_of_subcomponents in *; simpl in *;
                         ginv; eapply ind in run1; eauto; eauto 3 with eo));[].
        unfold call_prepare_already_in_log, bind in Heqx2; simpl in *; smash_minbft;
          try (complete (unfold state_of_subcomponents in *; simpl in *;
                         ginv; eapply ind in run1; eauto; eauto 3 with eo));[].
        unfold state_of_subcomponents in *; simpl in *; ginv.
        unfold invalid_prepare in *; smash_minbft.
        rewrite ui_in_log_log_new_commit in inlog ;simpl in *.
        unfold commit2ui_i in inlog; simpl in *.
        unfold commit_ui_j_rep_not_in_log in inlog; simpl in *.
        unfold commit2sender_j in inlog; simpl in *.
        unfold MinBFT_data_knows; simpl.
        applydup valid_prepare_implies_view in Heqx0 as eqv.
        rewrite eqv in inlog; autorewrite with minbft in *.
        rewrite prepare_not_already_in_log_implies_find_entry in inlog; auto;[].
        simpl in *; autorewrite with minbft in *.

        smash_minbft;[| |].

        { exists (prepare2hash_data p); simpl.
          unfold verify_UI in *; autorewrite with minbft in *.
          dands; auto;[].
          rewrite hash_data_in_log_log_new_commit_eq.
          unfold commit2hash_data_i; simpl.
          unfold commit_ui_j_rep_not_in_log; simpl.
          unfold commit2sender_j in *; simpl in *.
          unfold commit2hash_data_j; simpl.
          unfold RequestData2HashData; simpl in *.
          rewrite eqv; autorewrite with minbft.
          smash_minbft. }

        { rewrite ui_in_log_log_new_prepare in Heqx2; smash_minbft;[]; GC.
          eapply ind in run1; try exact Heqx2; try reflexivity; eauto 3 with eo.
          exrepnd.
          exists hd; dands; auto.
          unfold MinBFT_data_knows; simpl.
          rewrite hash_data_in_log_log_new_commit_eq; simpl.
          unfold commit2hash_data_i; simpl.
          unfold commit_ui_j_rep_not_in_log; simpl.
          unfold commit2sender_j in *; simpl in *.
          unfold commit2hash_data_j; simpl.
          unfold RequestData2HashData; simpl in *.
          rewrite eqv; autorewrite with minbft.
          rewrite prepare_not_already_in_log_implies_find_entry; auto;[].
          simpl in *; autorewrite with minbft.
          unfold MinBFT_data_knows in run1;simpl in run1.
          smash_minbft; allrw MinBFTprops0.not_over_or; repnd; tcsp; GC;
            try rewrite @hash_data_in_log_log_new_prepare in *; smash_minbft. }

        { exists (Build_HashData
                    (prepare2view p)
                    (request_b (prepare2request p))
                    (Build_preUI (usig_id s1) (S (usig_counter s1)))); simpl.
          autorewrite with minbft; dands; auto;[].
          allrw not_over_or; repnd; GC.
          Opaque UI_dec.
          rewrite @ui_in_log_log_new_prepare in *; simpl in *.
          smash_minbft;[]; GC.
          rewrite hash_data_in_log_log_new_commit_eq; simpl.
          unfold commit2hash_data_i; simpl.
          unfold commit_ui_j_rep_not_in_log; simpl.
          unfold commit2sender_j in *; simpl in *.
          unfold commit2hash_data_j; simpl.
          unfold RequestData2HashData; simpl in *.
          rewrite eqv; autorewrite with minbft.
          rewrite prepare_not_already_in_log_implies_find_entry; auto;[].
          simpl in *; autorewrite with minbft.
          smash_minbft. }
      }

      { Case "Commit".

        unfold call_verify_ui, bind in Heqx; simpl in *; smash_minbft;
          try (complete (unfold state_of_subcomponents in *; simpl in *;
                         ginv; eapply ind in run1; eauto; eauto 3 with eo));[].
        unfold call_prepare_already_in_log, bind_pair, bind in *; simpl in *; smash_minbft;
          try (complete (unfold state_of_subcomponents in *; simpl in *;
                         ginv; eapply ind in run1; eauto; eauto 3 with eo));[|].

        {
          unfold call_log_commit, bind in Heqx4; simpl in *; smash_minbft;
            try (complete (unfold state_of_subcomponents in *; simpl in *;
                           ginv; eapply ind in run1; eauto; eauto 3 with eo));[].
          unfold call_is_committed, bind in Heqx; simpl in *; smash_minbft;
            try (complete (unfold state_of_subcomponents in *; simpl in *;
                           ginv; eapply ind in run1; eauto; eauto 3 with eo));[|].

          { unfold state_of_subcomponents in *; simpl in *; ginv.
            rewrite ui_in_log_log_new_commit in inlog; smash_minbft;
              try (complete (eapply ind in run1; eauto; eauto 3 with eo));
              [| |].

            { exists (commit2hash_data_i c); simpl.
              unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
              dands; auto;[].
              unfold MinBFT_data_knows in *; simpl in *.
              rewrite hash_data_in_log_log_new_commit_eq; smash_minbft. }

            { eapply ind in run1; try exact Heqx; simpl in *;
                unfold state_of_subcomponents in *; simpl in *; try reflexivity;
                  eauto 3 with eo; exrepnd; exists hd; dands; auto.
              unfold MinBFT_data_knows in *; simpl in *.
              rewrite hash_data_in_log_log_new_commit_eq; smash_minbft. }

            { exists (commit2hash_data_j c).
              unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
              dands; auto;[].
              unfold MinBFT_data_knows in *; simpl in *.
              rewrite hash_data_in_log_log_new_commit_eq; smash_minbft. }
          }

          { unfold state_of_subcomponents in *; simpl in *; ginv.
            rewrite ui_in_log_log_new_commit in inlog; smash_minbft;
              try (complete (eapply ind in run1; eauto; eauto 3 with eo));
              [| |].

            { exists (commit2hash_data_i c); simpl.
              unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
              dands; auto;[].
              unfold MinBFT_data_knows in *; simpl in *.
              rewrite hash_data_in_log_log_new_commit_eq; smash_minbft. }

            { eapply ind in run1; try exact Heqx; simpl in *;
                unfold state_of_subcomponents in *; simpl in *; try reflexivity;
                  eauto 3 with eo; exrepnd; exists hd; dands; auto.
              unfold MinBFT_data_knows in *; simpl in *.
              rewrite hash_data_in_log_log_new_commit_eq; smash_minbft. }

            { exists (commit2hash_data_j c).
              unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
              dands; auto;[].
              unfold MinBFT_data_knows in *; simpl in *.
              rewrite hash_data_in_log_log_new_commit_eq; smash_minbft. }
          }
        }

        {
          unfold call_log_commit, bind in Heqx4; simpl in *; smash_minbft;
            try (complete (unfold state_of_subcomponents in *; simpl in *;
                           ginv; eapply ind in run1; eauto; eauto 3 with eo));[].
          unfold call_is_committed, bind in Heqx; simpl in *; smash_minbft;
            try (complete (unfold state_of_subcomponents in *; simpl in *;
                           ginv; eapply ind in run1; eauto; eauto 3 with eo));[|].

          { unfold state_of_subcomponents in *; simpl in *; ginv.
            rewrite ui_in_log_log_new_commit in inlog; smash_minbft;
              try (complete (eapply ind in run1; eauto; eauto 3 with eo));
              [| |].

            { exists (commit2hash_data_i c); simpl.
              unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
              dands; auto;[].
              unfold MinBFT_data_knows in *; simpl in *.
              rewrite hash_data_in_log_log_new_commit_eq; smash_minbft. }

            { rewrite ui_in_log_log_new_commit in Heqx; smash_minbft;
                try (complete (eapply ind in run1; eauto; eauto 3 with eo));
                [| |].

              { exists (commit2hash_data_i c); simpl.
                unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
                dands; auto;[].
                unfold MinBFT_data_knows in *; simpl in *.
                rewrite hash_data_in_log_log_new_commit_eq; smash_minbft. }

              { eapply ind in run1; try exact Heqx; simpl in *;
                  unfold state_of_subcomponents in *; simpl in *; try reflexivity;
                    eauto 3 with eo; exrepnd; exists hd; dands; auto.
                unfold MinBFT_data_knows in *; simpl in *.
                unfold commit2ui_i in *; simpl in *.
                autorewrite with minbft in *.
                rewrite hash_data_in_log_log_new_commit_eq; smash_minbft.
                { rewrite hash_data_in_log_log_new_commit_eq in Heqx; simpl in *.
                  unfold commit_ui_j_rep_not_in_log in *; simpl in *; smash_minbft. }
                { rewrite hash_data_in_log_log_new_commit_eq in Heqx; simpl in *.
                  unfold commit_ui_j_rep_not_in_log in *; simpl in *; smash_minbft. }
              }

              { exists (Build_HashData
                          (commit2view c)
                          (request_b (commit2request c))
                          (Build_preUI (usig_id s1) (S (usig_counter s1)))); simpl.
                unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
                dands; auto;[].
                unfold MinBFT_data_knows in *; simpl in *.
                rewrite hash_data_in_log_log_new_commit_eq; smash_minbft.
                { rewrite hash_data_in_log_log_new_commit_eq in Heqx; simpl in *.
                  unfold commit_ui_j_rep_not_in_log in *; simpl in *; smash_minbft. }
                { rewrite hash_data_in_log_log_new_commit_eq in Heqx; simpl in *.
                  unfold commit_ui_j_rep_not_in_log in *; simpl in *; smash_minbft. }
              }
            }

            { exists (commit2hash_data_j c).
              unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
              dands; auto;[].
              unfold MinBFT_data_knows in *; simpl in *.
              rewrite hash_data_in_log_log_new_commit_eq; smash_minbft. }
          }

          { unfold state_of_subcomponents in *; simpl in *; ginv.
            rewrite ui_in_log_log_new_commit in inlog; smash_minbft;
              try (complete (eapply ind in run1; eauto; eauto 3 with eo));
              [| |].

            { exists (commit2hash_data_i c); simpl.
              unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
              dands; auto;[].
              unfold MinBFT_data_knows in *; simpl in *.
              rewrite hash_data_in_log_log_new_commit_eq; smash_minbft. }

            { rewrite ui_in_log_log_new_commit in Heqx; smash_minbft;
                try (complete (eapply ind in run1; eauto; eauto 3 with eo));
                [| |].

              { exists (commit2hash_data_i c); simpl.
                unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
                dands; auto;[].
                unfold MinBFT_data_knows in *; simpl in *.
                rewrite hash_data_in_log_log_new_commit_eq; smash_minbft. }

              { eapply ind in run1; try exact Heqx; simpl in *;
                  unfold state_of_subcomponents in *; simpl in *; try reflexivity;
                    eauto 3 with eo; exrepnd; exists hd; dands; auto.
                unfold MinBFT_data_knows in *; simpl in *.
                unfold commit2ui_i in *; simpl in *.
                autorewrite with minbft in *.
                rewrite hash_data_in_log_log_new_commit_eq; smash_minbft.
                { rewrite hash_data_in_log_log_new_commit_eq in Heqx; simpl in *.
                  unfold commit_ui_j_rep_not_in_log in *; simpl in *; smash_minbft. }
                { rewrite hash_data_in_log_log_new_commit_eq in Heqx; simpl in *.
                  unfold commit_ui_j_rep_not_in_log in *; simpl in *; smash_minbft. }
              }

              { exists (Build_HashData
                          (commit2view c)
                          (request_b (commit2request c))
                          (Build_preUI (usig_id s1) (S (usig_counter s1)))); simpl.
                unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
                dands; auto;[].
                unfold MinBFT_data_knows in *; simpl in *.
                rewrite hash_data_in_log_log_new_commit_eq; smash_minbft.
                { rewrite hash_data_in_log_log_new_commit_eq in Heqx; simpl in *.
                  unfold commit_ui_j_rep_not_in_log in *; simpl in *; smash_minbft. }
                { rewrite hash_data_in_log_log_new_commit_eq in Heqx; simpl in *.
                  unfold commit_ui_j_rep_not_in_log in *; simpl in *; smash_minbft. }
              }
            }

            { exists (commit2hash_data_j c).
              unfold verify_UI in *; simpl in *; autorewrite with minbft in *.
              dands; auto;[].
              unfold MinBFT_data_knows in *; simpl in *.
              rewrite hash_data_in_log_log_new_commit_eq; smash_minbft. }
          }
        }
      }
    }
  Qed.*)

  Lemma are_procs_n_procs_minbft_subs_new :
    forall u l, are_procs_n_procs (MinBFTsubs_new u l).
  Proof.
    introv i; simpl in *; repndors; subst; tcsp;
      unfold is_proc_n_nproc; simpl; eauto 3 with minbft;
        unfold is_proc_n_proc; simpl; eexists; introv; try reflexivity.
  Qed.
  Hint Resolve are_procs_n_procs_minbft_subs_new : minbft.

  Lemma similar_minbft_implies_subs_new :
    forall (subs : n_procs 1) u l,
      similar_subs (MinBFTsubs_new u l) subs
      -> exists u' l', subs = MinBFTsubs_new u' l'.
  Proof.
    introv sim.
    inversion sim; subst; clear sim.
    inversion sims; subst; clear sims.
    inversion sims0; subst; clear sims0.
    applydup @similar_procs_implies_same_name in simp; simpl in *.
    applydup @similar_procs_implies_same_name in simp0; simpl in *.
    destruct p2, p0; simpl in *; subst; simpl in *.
    destruct pp_proc, pp_proc0; simpl in *; tcsp;[].
    apply @similar_procs_implies_same_proc in simp.
    apply @similar_procs_implies_same_proc in simp0.
    simpl in *; repnd; subst.
    destruct a, a0; simpl in *; subst; simpl in *; tcsp;[].
    unfold similar_sms_at in *; repnd; simpl in *; subst; tcsp.
    unfold MinBFTsubs_new, build_m_sm, build_mp_sm, at2sm; simpl; eauto.
  Qed.

  Lemma M_run_ls_on_input_ls_is_minbft_new :
    forall cn i o r s u l ls,
      M_run_ls_on_input (MinBFTlocalSys_new r s u l) cn i = (ls, o)
      -> exists s' u' l',
        ls = MinBFTlocalSys_new r s' u' l'.
  Proof.
    introv run.
    apply M_run_ls_on_input_ls_is_minbft_newP in run; eauto 3 with minbft; tcsp;
      try (complete (unfold get_names; simpl; introv xx; repndors; tcsp; inversion xx)).
    exrepnd; subst; simpl in *.
    apply similar_minbft_implies_subs_new in run1; exrepnd; subst.
    eexists; eexists; eexists; try reflexivity.
  Qed.

  Lemma request_data_was_verified :
    forall {eo : EventOrdering} (e : Event) (l : LOG_state) (u : TRINC_state) v r ui,
      is_replica e
      -> M_state_sys_on_event MinBFTsys e LOGname = Some l
      -> M_state_sys_on_event MinBFTsys e USIGname = Some u
      -> kc_knows (minbft_data_rdata (request_data v r ui)) l
      -> verify_hash_usig (Build_HashData v r (ui_pre ui)) (ui2digest ui) (trinc_local_keys u) = true.
  Proof.
    introv isr eqst1 eqst2 unl.

    unfold kc_Tknows in unl; simpl in unl.
    unfold MinBFT_data_knows in unl; simpl in unl.

    rewrite M_state_sys_on_event_unfold in eqst1.
    rewrite M_state_sys_on_event_unfold in eqst2.

    apply map_option_Some in eqst1.
    apply map_option_Some in eqst2.
    exrepnd; try rev_Some.

    rewrite eqst1 in eqst2; ginv.

    unfold is_replica in *; exrepnd.

    revert dependent u.
    revert dependent l.
    revert dependent a.
    rewrite isr0; simpl.

    (* WARNING *)
    clear isr0.

    induction e as [e ind] using predHappenedBeforeInd;[]; introv run stl inlog stu.

    rewrite M_run_ls_on_event_unroll2 in run.

    (*rewrite M_run_ls_before_event_unroll_on in run.

    destruct (dec_isFirst e) as [d|d].

    {
      clear ind.

      unfold M_run_ls_on_this_one_event in run; simpl in *.
      apply map_option_Some in run; exrepnd; rev_Some.
      autorewrite with minbft in *.

      Time minbft_dest_msg Case;
        repeat (simpl in *; autorewrite with minbft in *; smash_minbft2);
        ginv; simpl in *; autorewrite with minbft in *; auto;
          unfold verify_UI in *; simpl in *; autorewrite with minbft in *;
            first [destruct p as [b pui], b
                  |destruct c as [b pui], b]; simpl in *; ginv;
              unfold prepare2hash_data, RequestData2HashData, prepare2request in *; simpl in *; auto;
                unfold invalid_prepare, valid_prepare in *; simpl in *; smash_minbft;
                  unfold prepare2view in *; simpl in *; subst; tcsp;
                    try (complete (unfold state_of_subcomponents in *; simpl in *; ginv)).
    }*)

    {
      apply map_option_Some in run; exrepnd; rev_Some.
      applydup M_run_ls_before_event_ls_is_minbft in run1; exrepnd; subst.

      unfold M_run_ls_on_this_one_event in run0; simpl in *.
      apply map_option_Some in run0; exrepnd; rev_Some; minbft_simp.
      unfold M_run_ls_on_input_ls in *; simpl in *.
      remember (M_run_ls_on_input (MinBFTlocalSys_new r0 s s1 s2) (msg_comp_name 0) a0) as run.
      symmetry in Heqrun; repnd; simpl in *.
      applydup (M_run_ls_on_input_ls_is_minbft_new (msg_comp_name 0)) in Heqrun; exrepnd; subst; simpl in *.
      autorewrite with minbft in *; minbft_simp.
      unfold M_run_ls_on_input in Heqrun; simpl in *.
      autorewrite with minbft in *; simpl in *.

      Time minbft_dest_msg Case;
        repeat (simpl in *; autorewrite with minbft in *; smash_minbft2);
        try (simpl in *; unfold state_of_subcomponents in *; simpl in *; ginv);
        (unfold lower_out_break in *; simpl in *; minbft_simp;
                ginv; unfold try_create_trinc_ui, try_update_TRINC in *; simpl in *;
                  repeat (smash_minbft1; ginv; simpl in *;tcsp);
                  rewrite M_run_ls_before_event_unroll_on in run1;
                  destruct (dec_isFirst e); simpl in *;
                    minbft_simp; simpl in *; repeat (smash_minbft1; ginv; simpl in *;tcsp);
                      try (complete (eapply ind in run1; eauto; eauto 3 with eo));
                      first [destruct p as [b pui], b
                            |destruct c as [b pui], b]; simpl in *; ginv;
                        unfold prepare2hash_data, RequestData2HashData, prepare2request in *; simpl in *; auto;
                          unfold invalid_prepare, valid_prepare in *; simpl in *; smash_minbft3;
                            unfold prepare2view in *; simpl in *; subst; tcsp; ginv; auto).
    }
  Qed.

  Lemma M_run_ls_on_event_MinBFT_to_components :
    forall i {eo : EventOrdering} (e : Event) j s l u,
      loc e = MinBFT_replica i
      -> M_run_ls_on_event (MinBFTlocalSys i) e = Some (MinBFTlocalSys_new j s u l)
      -> M_state_sys_on_event MinBFTsys e MAINname = Some s
         /\ M_state_sys_on_event MinBFTsys e USIGname = Some u
         /\ M_state_sys_on_event MinBFTsys e LOGname = Some l.
  Proof.
    introv eqrep h.
    unfold M_state_sys_on_event; allrw; simpl.
    unfold M_state_ls_on_event.
    allrw; simpl.
    unfold state_of_component; simpl; tcsp.
  Qed.

End TrIncprops1.

author: veri-fit

repo: Asphalion

save_path: github-repos/coq/veri-fit-Asphalion


text:
(* -*- mode: coq; mode: visual-line -*-  *)
Require Import HoTT.Basics HoTT.Types.
Require Import HSet TruncType.
Require Import Truncations.Core.

Local Open Scope path_scope.

(** * Quotient of a Type by an hprop-valued relation

We aim to model:
<<
Inductive quotient : Type :=
   | class_of : A -> quotient
   | related_classes_eq : forall x y, (R x y), class_of x = class_of y
   | quotient_set : IsHSet quotient
>>
*)

(** This development should be further connected with the sections in the book; see below.*)

Module Export Quotient.

  Section Domain.

    Context {A : Type} (R : Relation A) {sR: is_mere_relation _ R}.

    (** We choose to let the definition of quotient depend on the proof that [R] is a set-relations.  Alternatively, we could have defined it for all relations and only develop the theory for set-relations.  The former seems more natural.

We do not require [R] to be an equivalence relation, but implicitly consider its transitive-reflexive closure. *)

    (** Note: If we wanted to be really accurate, we'd need to put [@quotient A R sr] in the max [U_{sup(i, j)}] of the universes of [A : U_i] and [R : A -> A -> U_j].  But this requires some hacky code, at the moment, and the only thing we gain is avoiding making use of an implicit hpropositional resizing "axiom". *)

    (** This definition has a parameter [sR] that shadows the ambient one in the Context in order to ensure that it actually ends up depending on everything in the Context when the section is closed, since its definition doesn't actually refer to any of them.  *)
    Private Inductive quotient {sR: is_mere_relation _ R} : Type :=
    | class_of : A -> quotient.

    (** The path constructors. *)
    Axiom related_classes_eq
    : forall {x y : A}, R x y ->
                        class_of x = class_of y.

    Axiom quotient_set : IsHSet (@quotient sR).
    Global Existing Instance quotient_set.

    Definition quotient_ind (P : (@quotient sR) -> Type) {sP : forall x, IsHSet (P x)}
               (dclass : forall x, P (class_of x))
               (dequiv : (forall x y (H : R x y), (related_classes_eq H) # (dclass x) = dclass y))
    : forall q, P q
      := fun q => match q with class_of a => fun _ _ => dclass a end sP dequiv.

    Definition quotient_ind_compute {P sP} dclass dequiv x
    : @quotient_ind P sP dclass dequiv (class_of x) = dclass x.
    Proof.
      reflexivity.
    Defined.

    (** Again equality of paths needs to be postulated *)
    Axiom quotient_ind_compute_path
    : forall P sP dclass dequiv,
      forall x y (H : R x y),
        apD (@quotient_ind P sP dclass dequiv) (related_classes_eq H)
        = dequiv x y H.

  End Domain.

End Quotient.

Section Equiv.

  Context `{Univalence}.

  Context {A : Type} (R : Relation A) {sR: is_mere_relation _ R}
          {Htrans : Transitive R} {Hsymm : Symmetric R}.

  Lemma quotient_path2 : forall {x y : quotient R} (p q : x=y), p=q.
  Proof.
    apply @hset_path2. apply _.
  Defined.

  Definition in_class : quotient R -> A -> HProp.
  Proof.
    refine (quotient_ind R (fun _ => A -> HProp) (fun a b => Build_HProp (R a b)) _).
    intros. eapply concat;[apply transport_const|].
    apply path_forall. intro z. apply path_hprop; simpl.
    apply @equiv_iff_hprop; eauto.
  Defined.

  Context {Hrefl : Reflexive R}.

  Lemma in_class_pr : forall x y, (in_class (class_of R x) y : Type) = R x y.
  Proof.
    reflexivity.
  Defined.

  Lemma quotient_ind_prop (P : quotient R -> Type)
        `{forall x, IsHProp (P x)} :
    forall dclass : forall x, P (class_of R x),
    forall q, P q.
  Proof.
    intros. apply (quotient_ind R P dclass).
    intros. apply path_ishprop.
  Defined.

  Global Instance decidable_in_class `{forall x y, Decidable (R x y)}
  : forall x a, Decidable (in_class x a).
  Proof.
    refine (quotient_ind_prop _ _).
    intros a b; exact (transport Decidable (in_class_pr a b) _).
  Defined.

  Lemma class_of_repr : forall q x, in_class q x -> q = class_of R x.
  Proof.
    apply (quotient_ind R
                        (fun q : quotient R => forall x, in_class q x -> q = class_of _ x)
                        (fun x y H => related_classes_eq R H)).
    intros.
    apply path_forall. intro z.
    apply path_forall;intro H'.
    apply quotient_path2.
  Defined.

  Lemma classes_eq_related : forall x y,
                               class_of R x = class_of R y -> R x y.
  Proof.
    intros x y H'.
    pattern (R x y).
    eapply transport.
    - apply in_class_pr.
    - pattern (class_of R x). apply (transport _ (H'^)).
      apply Hrefl.
  Defined.

  (** Thm 10.1.8 *)
  Theorem sets_exact : forall x y, (class_of R x = class_of R y) <~> R x y.
    intros ??. apply equiv_iff_hprop.
    - apply classes_eq_related.
    - apply related_classes_eq.
  Defined.

  Definition quotient_rec {B : Type} {sB : IsHSet B}
             (dclass : (forall x : A, B))
             (dequiv : (forall x y, R x y -> dclass x = dclass y))
  : quotient R -> B.
  Proof.
    apply (quotient_ind R (fun _ : quotient _ => B)) with dclass.
    intros ?? H'. destruct (related_classes_eq R H'). by apply dequiv.
  Defined.

  Definition quotient_rec2 {B : HSet} {dclass : (A -> A -> B)}:
    forall dequiv : (forall x x', R x x' -> forall y y',  R y y' ->
                                                          dclass x y = dclass x' y'),
      quotient R -> quotient R -> B.
  Proof.
    intro.
    assert (dequiv0 : forall x x0 y : A, R x0 y -> dclass x x0 = dclass x y)
      by (intros ? ? ? Hx; apply dequiv;[apply Hrefl|done]).
    refine (quotient_rec
              (fun x => quotient_rec (dclass x) (dequiv0 x)) _).
    intros x x' Hx.
    apply path_forall. red.
    assert (dequiv1 : forall y : A,
                        quotient_rec (dclass x) (dequiv0 x) (class_of _ y) =
                        quotient_rec (dclass x') (dequiv0 x') (class_of _ y))
      by (intros; by apply dequiv).
    refine (quotient_ind R (fun q =>
                              quotient_rec (dclass x) (dequiv0 x) q =
                              quotient_rec (dclass x') (dequiv0 x') q) dequiv1 _).
    intros. apply path_ishprop.
  Defined.

  Definition quotient_ind_prop' : forall P : quotient R -> Type,
                                  forall (Hprop' : forall x, IsHProp (P (class_of _ x))),
                                    (forall x, P (class_of _ x)) -> forall y, P y.
  Proof.
    intros ? ? dclass. apply quotient_ind with dclass.
    - simple refine (quotient_ind R (fun x => IsHSet (P x)) _ _); cbn beta; try exact _.
      intros; apply path_ishprop.
    - intros. apply Hprop'.
  Defined.

  (** From Ch6 *)
  Theorem quotient_surjective: IsSurjection (class_of R).
  Proof.
    apply BuildIsSurjection.
    apply (quotient_ind_prop (fun y => merely (hfiber (class_of R) y))); try exact _.
    intro x. apply tr. by exists x.
  Defined.

  (** From Ch10 *)
  Definition quotient_ump' (B:HSet): (quotient R -> B) ->
                                     (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0))).
    intro f. exists (compose f (class_of R) ).
    intros. f_ap. by apply related_classes_eq.
  Defined.

  Definition quotient_ump'' (B:HSet): (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0)))
                                      -> quotient R -> B.
    intros [f H'].
    apply (quotient_rec _ H').
  Defined.

  Theorem quotient_ump (B:HSet): (quotient R -> B) <~>
                                                   (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0))).
  Proof.
    refine (equiv_adjointify (quotient_ump' B) (quotient_ump'' B) _ _).
    - intros [f Hf].
      by apply equiv_path_sigma_hprop.
    - intros f.
      apply path_forall.
      red. apply quotient_ind_prop';[apply _|reflexivity].
  Defined.

  (** Missing

  The equivalence with VVquotient [A//R].

  This should lead to the unnamed theorem:

  10.1.10. Equivalence relations are effective and there is an equivalence [A/R<~>A//R]. *)

  (**
  The theory of canonical quotients is developed by C.Cohen:
  http://perso.crans.org/cohen/work/quotients/
 *)

End Equiv.

Section Functoriality.

  Definition quotient_functor
             {A : Type} (R : Relation A) {sR: is_mere_relation _ R}
             {B : Type} (S : Relation B) {sS: is_mere_relation _ S}
             (f : A -> B) (fresp : forall x y, R x y -> S (f x) (f y))
  : quotient R -> quotient S.
  Proof.
    refine (quotient_rec R (class_of S o f) _).
    intros x y r.
    apply related_classes_eq, fresp, r.
  Defined.

  Context {A : Type} (R : Relation A) {sR: is_mere_relation _ R}
          {B : Type} (S : Relation B) {sS: is_mere_relation _ S}.

  Global Instance quotient_functor_isequiv
             (f : A -> B) (fresp : forall x y, R x y <-> S (f x) (f y))
             `{IsEquiv _ _ f}
  : IsEquiv (quotient_functor R S f (fun x y => fst (fresp x y))).
  Proof.
    simple refine (isequiv_adjointify _ (quotient_functor S R f^-1 _)
                               _ _).
    - intros u v s.
      apply (snd (fresp _ _)).
      abstract (do 2 rewrite eisretr; apply s).
    - intros x; revert x; simple refine (quotient_ind S _ _ _).
      + intros b; simpl. apply ap, eisretr.
      + intros; apply path_ishprop.
    - intros x; revert x; simple refine (quotient_ind R _ _ _).
      + intros a; simpl. apply ap, eissect.
      + intros; apply path_ishprop.
  Defined.

  Definition quotient_functor_equiv
             (f : A -> B) (fresp : forall x y, R x y <-> S (f x) (f y))
             `{IsEquiv _ _ f}
  : quotient R <~> quotient S
    := Build_Equiv _ _
         (quotient_functor R S f (fun x y => fst (fresp x y))) _.

  Definition quotient_functor_equiv'
             (f : A <~> B) (fresp : forall x y, R x y <-> S (f x) (f y))
  : quotient R <~> quotient S
    := quotient_functor_equiv f fresp.

End Functoriality.

Section Kernel.

  (** ** Quotients of kernels of maps to sets give a surjection/mono factorization. *)

  Context {fs : Funext}.

  (** A function we want to factor. *)
  Context {A B : Type} `{IsHSet B} (f : A -> B).

  (** A mere relation equivalent to its kernel. *)
  Context (R : Relation A) {sR : is_mere_relation _ R}.
  Context (is_ker : forall x y, f x = f y <~> R x y).

  Theorem quotient_kernel_factor
  : exists (C : Type) (e : A -> C) (m : C -> B),
      IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e).
  Proof.
    pose (C := quotient R).
    (* We put this explicitly in the context so that typeclass resolution will pick it up. *)
    assert (IsHSet C) by (unfold C; apply _).
    exists C.
    pose (e := class_of R).
    exists e.
    transparent assert (m : (C -> B)).
    { apply quotient_ind with f; try exact _.
      intros x y H. transitivity (f x).
      - apply transport_const.
      - exact ((is_ker x y) ^-1 H). }
    exists m.
    split;[split;[split|]|].
    - assumption.
    - apply quotient_surjective.
    - intro u.
      apply hprop_allpath.
      assert (H : forall (x y : C) (p : m x = u) (p' : m y = u), x = y).
      { simple refine (quotient_ind R _ _ _).
        - intro a.
          simple refine (quotient_ind R _ _ _).
          + intros a' p p'; fold e in p, p'.
            * apply related_classes_eq.
              refine (is_ker a a' _).
              change (m (e a) = m (e a')).
              exact (p @ p'^).
          + intros; apply path_ishprop.
        - intros; apply path_ishprop. }
      intros [x p] [y p'].
      apply path_sigma_hprop; simpl.
      exact (H x y p p').
    - reflexivity.
  Defined.

End Kernel.

author: HoTT

repo: Coq-HoTT

save_path: github-repos/coq/HoTT-Coq-HoTT