text:
Require Import Coq.Lists.List.
Import ListNotations.

Require Import Tactics.
Require Import Axioms.
Require Import Sigma.
Require Import Equality.
Require Import Sequence.
Require Import Relation.
Require Import Ordinal.
Require Import Syntax.
Require Import SimpSub.
Require Import Dynamic.
Require Import Ofe.
Require Import Uniform.
Require Import Intensional.
Require Import Candidate.
Require Import System.
Require Import Semantics.
Require Import SemanticsKnot.
Require Import Judgement.
Require Import Hygiene.
Require Import ProperClosed.
Require Import ProperFun.
Require Import Shut.

Require Import Spaces.
Require Import Extend.
Require Import ProperLevel.
Require Import Urelsp.
Require Import Ceiling.
Require Import Equivalence.
Require Import Equivalences.
Require Import Truncate.
Require Import ProperDownward.
Require Import ProperLevel.
Require Import ProperEquiv.
Require Import Subsumption.
Require Import SemanticsPi.
Require Import SemanticsSigma.
Require Import ContextHygiene.
Require Import SoundUtil.

Lemma sound_sigma_formation :
  forall G a a' b b',
    pseq G (deqtype a a')
    -> pseq (cons (hyp_tm a) G) (deqtype b b')
    -> pseq G (deqtype (sigma a b) (sigma a' b')).
Proof.
intros G a b c d.
revert G.
refine (seq_pseq 2 [hyp_emp] c [hyp_emp] d 2 [] _ [_] _ _ _); cbn.
intros G Hclc Hcld Hseqab Hseqcd.
rewrite -> seq_eqtype in Hseqab, Hseqcd |- *.
intros i s s' Hs.
so (seqctx_impl_closub _#4 (pwctx_impl_seqctx _#4 Hs)) as (Hcls & Hcls').
so (Hseqab _#3 Hs) as (A & Hal & Har & Hbl & Hbr).
assert (den A = ceiling (S i) (den A)) as HeqA.
  {
  so (basic_impl_iutruncate _#6 Hal) as Heq.
  exact (f_equal den Heq).
  }
exploit (extract_functional_multi toppg i (den A) (subst (under 1 s) c) (subst (under 1 s') c) (subst (under 1 s) d) (subst (under 1 s') d)) as (C & Hcl & Hcr & Hdl & Hdr); eauto using subst_closub_under_permit.
  {
  intros j m p Hmp.
  assert (pwctx j (dot m s) (dot p s') (cons (hyp_tm a) G)) as Hss.
    {
    assert (j <= i) as Hj.
      {
      rewrite -> HeqA in Hmp.
      destruct Hmp.
      omega.
      }
    apply pwctx_cons_tm_seq; eauto using pwctx_downward.
      {
      eapply seqhyp_tm_leq; eauto using interp_increase, toppg_max.
      }

      {
      intros j' t t' Ht.
      so (Hseqab _#3 Ht) as (R & Hl & Hr & _).
      eauto.
      }
    }
  so (Hseqcd _#3 Hss) as (R & Hcl & Hcr & Hdl & Hdr).
  exists R.
  simpsub.
  auto.
  }
exists (iusigma stop A C).
simpsub.
do2 3 split; auto;
apply interp_eval_refl;
apply interp_sigma; auto.
Qed.

Lemma sound_sigma_formation_univ :
  forall G lv a a' b b',
    pseq G (deq a a' (univ lv))
    -> pseq (cons (hyp_tm a) G) (deq b b' (univ (subst sh1 lv)))
    -> pseq G (deq (sigma a b) (sigma a' b') (univ lv)).
Proof.
intros G lv a b c d.
revert G.
refine (seq_pseq 2 [hyp_emp] c [hyp_emp] d 2 [] _ [_] _ _ _); cbn.
intros G Hclc Hcld Hseqab Hseqcd.
rewrite -> seq_univ in Hseqab, Hseqcd |- *.
intros i s s' Hs.
so (seqctx_impl_closub _#4 (pwctx_impl_seqctx _#4 Hs)) as (Hcls & Hcls').
so (Hseqab _#3 Hs) as (pg & A & Hlvl & Hlvr & Hal & Har & Hbl & Hbr).
assert (den A = ceiling (S i) (den A)) as HeqA.
  {
  so (basic_impl_iutruncate _#6 Hal) as Heq.
  exact (f_equal den Heq).
  }
exploit (extract_functional_multi pg i (den A) (subst (under 1 s) c) (subst (under 1 s') c) (subst (under 1 s) d) (subst (under 1 s') d)) as (C & Hcl & Hcr & Hdl & Hdr); eauto using subst_closub_under_permit.
  {
  intros j m p Hmp.
  assert (pwctx j (dot m s) (dot p s') (cons (hyp_tm a) G)) as Hss.
    {
    assert (j <= i) as Hj.
      {
      rewrite -> HeqA in Hmp.
      destruct Hmp.
      omega.
      }
    apply pwctx_cons_tm_seq; eauto using pwctx_downward.
      {
      eapply seqhyp_tm_leq; eauto using interp_increase, toppg_max.
      }

      {
      intros j' t t' Ht.
      so (Hseqab _#3 Ht) as (pg' & R & _ & _ & Hl & Hr & _).
      eauto.
      }
    }
  so (Hseqcd _#3 Hss) as (pg' & R & Hlvl' & _ & Hcl & Hcr & Hdl & Hdr).
  simpsubin Hlvl'.
  so (pginterp_fun _#3 Hlvl Hlvl'); subst pg'.
  exists R.
  simpsub.
  auto.
  }
exists pg, (iusigma stop A C).
simpsub.
do2 5 split; auto;
apply interp_eval_refl;
apply interp_sigma; auto.
Qed.

Local Ltac prove_hygiene :=
  repeat (first [ eapply subst_closub; eauto
                | apply closub_dot
                | apply hygiene_auto; cbn; repeat2 split; auto
                ]);
  eauto using hygiene_weaken, clo_min, hygiene_shift', hygiene_subst1;
  try (apply hygiene_var; cbn; auto; done).

Lemma sound_sigma_intro :
  forall G a b m m' n n',
    pseq G (deq m m' a)
    -> pseq G (deq n n' (subst1 m b))
    -> pseq (cons (hyp_tm a) G) (deqtype b b)
    -> pseq G (deq (ppair m n) (ppair m' n') (sigma a b)).
Proof.
intros G a b m n p q.
revert G.
refine (seq_pseq 5 [hyp_emp] b [] m [] p [] n [] q 3 [] _ [] _ [_] _ _ _); cbn.
intros G Hclb Hclm Hclp Hcln Hclq Hseqmn Hseqpq Hseqb.
rewrite -> seq_eqtype in Hseqb.
rewrite -> seq_deq in Hseqmn, Hseqpq |- *.
intros i s s' Hs.
so (pwctx_impl_closub _#4 Hs) as (Hcls & Hcls').
so (Hseqmn _#3 Hs) as (A & Hal & Har & Hm & Hn & Hmn).
so (Hseqpq _#3 Hs) as (R & Hmbl & Hmbr & Hp & Hq & Hpq); clear Hseqpq.
exploit (extract_functional toppg i (den A) (subst (under 1 s) b) (subst (under 1 s') b)) as H; eauto using subst_closub_under_permit.
  {
 exact (f_equal den (basic_impl_iutruncate _#6 Hal)).
  }

  {
  intros j r t Hrt.
  so (basic_member_index _#9 Hal Hrt) as Hj.
  assert (pwctx j (dot r s) (dot t s') (cons (hyp_tm a) G)) as Hs'.
    {
    apply pwctx_cons_tm_seq; eauto using pwctx_downward.
      {
      apply (seqhyp_tm _#5 (iutruncate (S j) A)).
        {
        eapply basic_downward; eauto.
        }

        {
        eapply basic_downward; eauto.
        }

        {
        split; auto.
        }
      }

      {
      intros j' u u' Hu.
      so (Hseqmn _#3 Hu) as (Q & Hl & Hr & _).
      eauto.
      }
    }
  so (Hseqb _#3 Hs') as (Q & Hl & Hr & _).
  exists Q.
  simpsub.
  auto.
  }
destruct H as (B & Hbl & Hbr).
exists (iusigma stop A B).
simpsub.
invert Hbl.
intros _ _ Hact.
so (Hact _#3 (le_refl _) Hm) as H.
simpsubin H.
simpsubin Hmbl.
so (basic_fun _#7 H Hmbl); clear H; subst R.
do2 4 split.
  {
  apply interp_eval_refl.
  apply interp_sigma; auto.
  }

  {
  apply interp_eval_refl.
  apply interp_sigma; auto.
  }

  {
  exists (subst s m), (subst s' m), (subst s p), (subst s' p), Hm.
  do2 4 split; auto using star_refl; try prove_hygiene.
  }

  {
  exists (subst s n), (subst s' n), (subst s q), (subst s' q), Hn.
  do2 4 split; auto using star_refl; try prove_hygiene.
  cbn.
  force_exact Hq.
  f_equal; f_equal; f_equal.
  apply urelspinj_equal; auto.
  }

  {
  exists (subst s m), (subst s' n), (subst s p), (subst s' q), Hmn.
  do2 4 split; auto using star_refl; try prove_hygiene.
  cbn.
  force_exact Hpq.
  f_equal; f_equal; f_equal.
  apply urelspinj_equal; auto.
  }
Qed.

Lemma sound_sigma_elim1 :
  forall G a b m n,
    pseq G (deq m n (sigma a b))
    -> pseq G (deq (ppi1 m) (ppi1 n) a).
Proof.
intros G a b m n.
revert G.
refine (seq_pseq 2 [] m [] n 1 [] _ _ _); cbn.
intros G Hclm Hcln Hseqmn.
rewrite -> seq_deq in Hseqmn |- *.
intros i s s' Hs.
so (pwctx_impl_closub _#4 Hs) as (Hcls & Hcls').
so (Hseqmn _#3 Hs) as (R & Hl & Hr & Hm & Hn & Hmn).
simpsubin Hl.
simpsubin Hr.
invert (basic_value_inv _#6 value_sigma Hl).
intros A B Hal Hbl Heq1.
invert (basic_value_inv _#6 value_sigma Hr).
intros A' B' Har Hbr Heq2.
so (eqtrans Heq1 (eqsymm Heq2)) as Heq.
clear Heq2.
subst R.
so (iusigma_inj _#5 Heq) as H.
injectionT H.
intros <-.
injectionT H.
intros <-.
exists A.
simpsub.
do2 4 split; auto.
  {
  destruct Hm as (p & q & r & t & Hpq & _ & _ & Hsteps & Hsteps' & Hrt).
  apply (urel_equiv _#3 p _ q); auto; prove_hygiene.
    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi1); auto using step_ppi11.
      exact Hsteps.
      }
    apply star_one; apply step_ppi12.
    }

    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi1); auto using step_ppi11.
      exact Hsteps'.
      }
    apply star_one; apply step_ppi12.
    }
  }

  {
  destruct Hn as (p & q & r & t & Hpq & _ & _ & Hsteps & Hsteps' & Hrt).
  apply (urel_equiv _#3 p _ q); auto; prove_hygiene.
    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi1); auto using step_ppi11.
      exact Hsteps.
      }
    apply star_one; apply step_ppi12.
    }

    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi1); auto using step_ppi11.
      exact Hsteps'.
      }
    apply star_one; apply step_ppi12.
    }
  }

  {
  destruct Hmn as (p & q & r & t & Hpq & _ & _ & Hsteps & Hsteps' & Hrt).
  apply (urel_equiv _#3 p _ q); auto; prove_hygiene.
    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi1); auto using step_ppi11.
      exact Hsteps.
      }
    apply star_one; apply step_ppi12.
    }

    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi1); auto using step_ppi11.
      exact Hsteps'.
      }
    apply star_one; apply step_ppi12.
    }
  }
Qed.

Lemma sound_sigma_elim2 :
  forall G a b m n,
    pseq G (deq m n (sigma a b))
    -> pseq G (deq (ppi2 m) (ppi2 n) (subst1 (ppi1 m) b)).
Proof.
intros G a b m n.
revert G.
refine (seq_pseq 3 [hyp_emp] b [] m [] n 1 [] _ _ _); cbn.
intros G Hclb Hclm Hlcn Hseqmn.
rewrite -> seq_deq in Hseqmn |- *.
intros i s s' Hs.
so (pwctx_impl_closub _#4 Hs) as (Hcls & Hcls').
so (Hseqmn _#3 Hs) as (R & Hl & Hr & Hm & Hn & Hmn).
simpsubin Hl.
simpsubin Hr.
invert (basic_value_inv _#6 value_sigma Hl).
intros A B Hal Hbl Heq1.
invert (basic_value_inv _#6 value_sigma Hr).
intros A' B' Har Hbr Heq2.
so (eqtrans Heq1 (eqsymm Heq2)) as Heq.
clear Heq2.
subst R.
so (iusigma_inj _#5 Heq) as H; clear Heq.
injectionT H.
intros <-.
injectionT H.
intros <-.
destruct Hm as (p1 & q1 & p2 & q2 & Hpq1 & _ & _ & Hstepsm & Hstepsm' & Hpq2).
cbn in Hpq2.
destruct Hn as (r1 & t1 & r2 & t2 & Hrt1 & _ & _ & Hstepsn & Hstepsn' & Hrt2).
cbn in Hrt2.
destruct Hmn as (p1' & q1' & r2' & t2' & Hpt1 & _ & _ & Hstepsma & Hstepsna' & Hpt2).
cbn in Hpt2.
injection (determinism_eval _#4 (conj Hstepsm value_ppair) (conj Hstepsma value_ppair)).
intros <- <-.
injection (determinism_eval _#4 (conj Hstepsn' value_ppair) (conj Hstepsna' value_ppair)).
intros <- <-.
exists (pi1 B (urelspinj (den A) _#3 Hpq1)).
simpsub.
do2 4 split.
  {
  invert Hbl.
  intros _ _ Hact.
  so (Hact _#3 (le_refl _) Hpq1) as H.
  simpsubin H.
  refine (basic_equiv _#7 _ _ H); clear H; try prove_hygiene.
  apply equiv_symm.
  apply equiv_funct; auto using equiv_refl.
  apply equivsub_dot; auto using equivsub_refl.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi1); auto using step_ppi11.
    exact Hstepsm.
    }
  apply star_one; apply step_ppi12.
  }

  {
  invert Hbr.
  intros _ _ Hact.
  so (Hact _#3 (le_refl _) Hpq1) as H.
  simpsubin H.
  refine (basic_equiv _#7 _ _ H); clear H; try prove_hygiene.
  apply equiv_symm.
  apply equiv_funct; auto using equiv_refl.
  apply equivsub_dot; auto using equivsub_refl.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi1); auto using step_ppi11.
    exact Hstepsm'.
    }
  apply star_one; apply step_ppi12.
  }

  {
  refine (urel_equiv _#7 _#4 Hpq2); try prove_hygiene.
    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi2); auto using step_ppi21.
      exact Hstepsm.
      }
    apply star_one; apply step_ppi22.
    }

    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi2); auto using step_ppi21.
      exact Hstepsm'.
      }
    apply star_one; apply step_ppi22.
    }
  }

  {
  refine (rel_from_dist _#6 _ (urel_equiv _#7 _#4 Hrt2)); try prove_hygiene.
    {
    apply dist_refl'.
    f_equal; f_equal.
    apply urelspinj_equal; auto.
    apply (urel_zigzag _#4 t1 p1); auto.
    }

    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi2); auto using step_ppi21.
      exact Hstepsn.
      }
    apply star_one; apply step_ppi22.
    }

    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi2); auto using step_ppi21.
      exact Hstepsn'.
      }
    apply star_one; apply step_ppi22.
    }
  }

  {
  refine (rel_from_dist _#6 _ (urel_equiv _#7 _#4 Hpt2)); try prove_hygiene.
    {
    apply dist_refl'.
    f_equal; f_equal.
    apply urelspinj_equal; auto.
    }

    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi2); auto using step_ppi21.
      exact Hstepsm.
      }
    apply star_one; apply step_ppi22.
    }

    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi2); auto using step_ppi21.
      exact Hstepsn'.
      }
    apply star_one; apply step_ppi22.
    }
  }
Qed.

Lemma sound_sigma_eta :
  forall G a b m,
    pseq G (deq m m (sigma a b))
    -> pseq G (deq m (ppair (ppi1 m) (ppi2 m)) (sigma a b)).
Proof.
intros G a b m.
revert G.
refine (seq_pseq 2 [hyp_emp] b [] m 1 [] _ _ _); cbn.
intros G Hclb Hclm Hseqm.
rewrite -> seq_deq in Hseqm |- *.
intros i s s' Hs.
so (pwctx_impl_closub _#4 Hs) as (Hcls & Hcls').
so (Hseqm _#3 Hs) as (R & Habl & Habr & Hm & _).
exists R.
do2 2 split; auto.
simpsub.
split; auto.
simpsubin Habl.
invert (basic_value_inv _#6 value_sigma Habl).
intros A B Ha Hb <-.
cbn in Hm.
decompose Hm.
intros n n' p p' Hn _ _ Hsteps Hsteps' Hp.
split.
  {
  assert (rel (den A) i (ppi1 (subst s m)) (ppi1 (subst s' m))) as Hn'.
    {
    eapply urel_equiv; eauto; try prove_hygiene.
      {
      apply equiv_symm.
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hsteps.
        }
      apply star_one; apply step_ppi12.
      }

      {
      apply equiv_symm.
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hsteps'.
        }
      apply star_one; apply step_ppi12.
      }
    }
  exists (ppi1 (subst s m)), (ppi1 (subst s' m)), (ppi2 (subst s m)), (ppi2 (subst s' m)), Hn'.
  do2 4 split; auto using star_refl; try prove_hygiene.
  cbn.
  refine (rel_from_dist _#6 _ (urel_equiv _#7 _#4 Hp)); try prove_hygiene.
    {
    apply dist_refl'.
    f_equal; f_equal.
    apply urelspinj_equal.
    apply (urel_zigzag _#4 n' (ppi1 (subst s m))); auto.
    eapply urel_equiv_1; eauto; try prove_hygiene.
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi1); auto using step_ppi11.
      exact Hsteps.
      }
    apply star_one; apply step_ppi12.
    }

    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi2); auto using step_ppi21.
      exact Hsteps.
      }
    apply star_one; apply step_ppi22.
    }

    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi2); auto using step_ppi21.
      exact Hsteps'.
      }
    apply star_one; apply step_ppi22.
    }
  }

  {
  assert (rel (den A) i n (ppi1 (subst s' m))) as Hn'.
    {
    eapply urel_equiv_2; eauto; try prove_hygiene.
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi1); auto using step_ppi11.
      exact Hsteps'.
      }
    apply star_one; apply step_ppi12.
    }
  exists n, (ppi1 (subst s' m)), p, (ppi2 (subst s' m)), Hn'.
  do2 4 split; auto using star_refl; try prove_hygiene.
  cbn.
  refine (rel_from_dist _#6 _ (urel_equiv_2 _#6 _ _ Hp)); try prove_hygiene.
    {
    apply dist_refl'.
    f_equal; f_equal.
    apply urelspinj_equal.
    apply (urel_zigzag _#4 n' (ppi1 (subst s m))); auto.
      {
      eapply urel_equiv_1; eauto; try prove_hygiene.
      apply equiv_symm.
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hsteps.
        }
      apply star_one; apply step_ppi12.
      }

      {
      refine (urel_equiv _#7 _ _ _ _ Hn); try prove_hygiene.
        {
        apply equiv_symm.
        apply steps_equiv.
        eapply star_trans.
          {
          apply (star_map' _ _ ppi1); auto using step_ppi11.
          exact Hsteps.
          }
        apply star_one; apply step_ppi12.
        }

        {
        apply equiv_symm.
        apply steps_equiv.
        eapply star_trans.
          {
          apply (star_map' _ _ ppi1); auto using step_ppi11.
          exact Hsteps'.
          }
        apply star_one; apply step_ppi12.
        }
      }
    }

    {
    apply equiv_symm.
    apply steps_equiv.
    eapply star_trans.
      {
      apply (star_map' _ _ ppi2); auto using step_ppi21.
      exact Hsteps'.
      }
    apply star_one; apply step_ppi22.
    }
  }
Qed.

Lemma sound_sigma_eta_hyp :
  forall G1 G2 a b m n c,
    pseq (substctx (dot (ppair (var 1) (var 0)) (sh 2)) G2 ++ cons (hyp_tm b) (cons (hyp_tm a) G1)) (deq m n (subst (under (length G2) (dot (ppair (var 1) (var 0)) (sh 2))) c))
    -> pseq (G2 ++ cons (hyp_tm (sigma a b)) G1) (deq (subst (under (length G2) (dot (ppi2 (var 0)) (dot (ppi1 (var 0)) sh1))) m) (subst (under (length G2) (dot (ppi2 (var 0)) (dot (ppi1 (var 0)) sh1))) n) c).
Proof.
intros G1 G2 a b m n c.
revert G1.
refine (seq_pseq_hyp 2 [hyp_emp] b (G2 ++ [hyp_tm (sigma a b)]) c 1 _ [_; _] _ _ [_] _ _); cbn.
intros G1 Hclb Hclc Hseq _.
eapply subsume_seq_extract; eauto; clear Hseq.
  {
  autorewrite with canonlist in Hclc.
  auto.
  }
apply subsume_under.
do2 2 split.
  {
  intros j.
  split.
    {
    intro Hj.
    destruct j as [| [| j]]; simpsub; prove_hygiene.
    }

    {
    intro Hj.
    rewrite -> ctxpred_length.
    cbn.
    destruct j as [| j]; try omega.
    simpsubin Hj.
    rewrite -> ctxpred_length in Hj.
    cbn in Hj.
    invert Hj; intro; omega.
    }
  }

  {
  intros j.
  split.
    {
    intro Hj.
    destruct j as [| [| j]]; simpsub; prove_hygiene.
    }

    {
    intro Hj.
    rewrite -> ctxpred_length.
    cbn.
    destruct j as [| [| j]]; try omega.
    simpsubin Hj.
    rewrite -> ctxpred_length in Hj.
    cbn in Hj.
    invert Hj; intro; omega.
    }
  }
intros i ss ss' Hss.
invertc Hss.
intros p q s s' Hs Hpq Hleft Hright <- <-.
so (pwctx_impl_closub _#4 Hs) as (Hcls & Hcls').
simpsubin Hpq.
invertc Hpq.
intros R Habl Habr Hpq.
invert (basic_value_inv _#6 value_sigma Habl).
intros A B Hal Hbl Heq1.
invert (basic_value_inv _#6 value_sigma Habr).
intros A' B' Har Hbr Heq2.
so (eqtrans Heq1 (eqsymm Heq2)) as Heq.
clear Heq2.
subst R.
so (iusigma_inj _#5 Heq) as H; clear Heq.
injectionT H.
intros <-.
injectionT H.
intros <-.
destruct Hpq as (p1 & q1 & p2 & q2 & Hpq1 & Hclp & Hclq & Hstepsp & Hstepsq & Hpq2).
do2 4 split.
  {
  simpsub.
  apply pwctx_cons_tm.
    {
    apply pwctx_cons_tm; auto.
      {
      apply (seqhyp_tm _#5 A); auto.
      eapply urel_equiv; eauto; try prove_hygiene.
        {
        apply equiv_symm.
        apply steps_equiv.
        eapply star_trans.
          {
          apply (star_map' _ _ ppi1); auto using step_ppi11.
          exact Hstepsp.
          }
        apply star_one; apply step_ppi12.
        }

        {
        apply equiv_symm.
        apply steps_equiv.
        eapply star_trans.
          {
          apply (star_map' _ _ ppi1); auto using step_ppi11.
          exact Hstepsq.
          }
        apply star_one; apply step_ppi12.
        }
      }

      {
      intros j u Hj Hu.
      exploit (Hleft j false u) as H; auto using smaller_le, pwctx_impl_seqctx.
      rewrite -> qpromote_hyp_tm in H.
      simpsubin H.
      invertc H.
      intros R Hl Hr.
      invert (basic_value_inv _#6 value_sigma Hl); clear Hl.
      intros A' B' Har' _ Heq1.
      invert (basic_value_inv _#6 value_sigma Hr); clear Hr.
      intros A'' B'' Har'' _ Heq2.
      so (eqtrans Heq1 (eqsymm Heq2)) as Heq.
      clear Heq2.
      subst R.
      so (basic_fun _#7 (basic_downward _#7 Hj Har) Har'); subst A'.
      so (iusigma_inj _#5 Heq) as H; clear Heq.
      injectionT H.
      intros <-.
      clear H.
      apply (relhyp_tm _#4 (iutruncate (S j) A)); auto.
      }

      {
      intros j u Hj Hu.
      exploit (Hright j false u) as H; auto using smaller_le, pwctx_impl_seqctx.
      rewrite -> qpromote_hyp_tm in H.
      simpsubin H.
      invertc H.
      intros R Hl Hr.
      invert (basic_value_inv _#6 value_sigma Hl); clear Hl.
      intros A' B' Hal' _ Heq1.
      invert (basic_value_inv _#6 value_sigma Hr); clear Hr.
      intros A'' B'' Hal'' _ Heq2.
      so (eqtrans Heq1 (eqsymm Heq2)) as Heq.
      clear Heq2.
      subst R.
      so (basic_fun _#7 (basic_downward _#7 Hj Hal) Hal'); subst A'.
      so (iusigma_inj _#5 Heq) as H; clear Heq.
      injectionT H.
      intros <-.
      clear H.
      apply (relhyp_tm _#4 (iutruncate (S j) A)); auto.
      }
    }

    {
    apply (seqhyp_tm _#5 (pi1 B (urelspinj (den A) _#3 Hpq1))).
      {
      invert Hbl.
      intros _ _ Hact.
      so (Hact _#3 (le_refl _) Hpq1) as H.
      simpsubin H.
      eapply basic_equiv; eauto; clear H; try prove_hygiene.
      apply equiv_symm.
      apply equiv_funct; auto using equiv_refl.
      apply equivsub_dot; auto using equivsub_refl.
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hstepsp.
        }
      apply star_one; apply step_ppi12.
      }

      {
      invert Hbr.
      intros _ _ Hact.
      so (Hact _#3 (le_refl _) Hpq1) as H.
      simpsubin H.
      eapply basic_equiv; eauto; clear H; try prove_hygiene.
      apply equiv_symm.
      apply equiv_funct; auto using equiv_refl.
      apply equivsub_dot; auto using equivsub_refl.
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hstepsq.
        }
      apply star_one; apply step_ppi12.
      }

      {
      eapply urel_equiv; eauto; try prove_hygiene.
        {
        apply equiv_symm.
        apply steps_equiv.
        eapply star_trans.
          {
          apply (star_map' _ _ ppi2); auto using step_ppi21.
          exact Hstepsp.
          }
        apply star_one; apply step_ppi22.
        }

        {
        apply equiv_symm.
        apply steps_equiv.
        eapply star_trans.
          {
          apply (star_map' _ _ ppi2); auto using step_ppi21.
          exact Hstepsq.
          }
        apply star_one; apply step_ppi22.
        }
      }
    }

    {
    intros j uu Hj Huu.
    invertc Huu.
    intros r u Hu Hr _ _ <-.
    so (pwctx_impl_closub _#4 Hu) as (_ & Hclu).
    simpsubin Hr.
    invertc Hr.
    intros A' Hal' Hau Hr.
    so (basic_fun _#7 (basic_downward _#7 Hj Hal) Hal'); subst A'.
    clear Hal'.
    so (urel_closed _#5 Hr) as (_ & Hclr).
    exploit (Hleft j false u) as H; auto using smaller_le, pwctx_impl_seqctx.
    rewrite -> qpromote_hyp_tm in H.
    simpsubin H.
    invertc H.
    intros R H1 H2.
    invert (basic_value_inv _#6 value_sigma H1); clear H1.
    intros A' B' Har' Hbr' Heq1.
    invert (basic_value_inv _#6 value_sigma H2); clear H2.
    intros A'' B'' Har'' Hbr'' Heq2.
    so (eqtrans Heq1 (eqsymm Heq2)) as Heq.
    clear Heq2.
    subst R.
    so (iusigma_inj _#5 Heq) as H; clear Heq.
    injectionT H.
    intros <-.
    injectionT H.
    intros <-.
    so (basic_fun _#7 (basic_downward _#7 Hj Har) Har'); subst A'.
    so (functional_fun _#8 (functional_downward _#8 Hj Hbr) Hbr'); subst B'.
    apply (relhyp_tm _#4 (iutruncate (S j) (pi1 B (embed_ceiling _ _ (urelspinj (ceiling (S j) (den A)) _#3 (conj (Nat.lt_succ_diag_r j) (urel_downward_leq _#6 Hj Hpq1))))))).
      {
      invert Hbr'.
      intros B' _ _ Hact Heq.
      so (eq_dep_impl_eq_snd _#5 Heq); subst B'; clear Heq.
      so (Hact _#3 (le_refl _) (conj (Nat.lt_succ_diag_r j) (urel_downward_leq _#6 Hj Hpq1))) as H.
      cbn in H.
      eapply basic_equiv; eauto; clear H; try prove_hygiene.
      simpsub.
      apply equiv_symm.
      apply equiv_funct; auto using equiv_refl.
      apply equivsub_dot; auto using equivsub_refl.
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hstepsq.
        }
      apply star_one; apply step_ppi12.
      }

      {
      invert Hbr''.
      intros B' _ _ Hact Heq.
      so (eq_dep_impl_eq_snd _#5 Heq); subst B'; clear Heq.
      so (Hact _#3 (le_refl _) Hr) as H.
      cbn in H.
      rewrite -> embed_ceiling_urelspinj.
      destruct Hr as (Hj' & Hr).
      rewrite -> embed_ceiling_urelspinj in H.
      simpsubin H.
      force_exact H.
      unfold interp.
      f_equal.
      f_equal; f_equal.
      apply urelspinj_equal.
      refine (urel_equiv_1 _#6 _ _ (urel_downward_leq _#6 Hj Hpq1)); try prove_hygiene.
      apply equiv_symm.
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hstepsp.
        }
      apply star_one; apply step_ppi12.
      }
    }

    {
    intros j uu Hj Huu.
    invertc Huu.
    intros r u Hu Hr _ _ <-.
    so (pwctx_impl_closub _#4 Hu) as (Hclu & _).
    simpsubin Hr.
    invertc Hr.
    intros A' Hau Har' Hr.
    so (basic_fun _#7 (basic_downward _#7 Hj Har) Har'); subst A'.
    clear Har'.
    so (urel_closed _#5 Hr) as (Hclr & _).
    exploit (Hright j false u) as H; auto using smaller_le, pwctx_impl_seqctx.
    rewrite -> qpromote_hyp_tm in H.
    simpsubin H.
    invertc H.
    intros R H1 H2.
    invert (basic_value_inv _#6 value_sigma H1); clear H1.
    intros A' B' Hal' Hbl' Heq1.
    invert (basic_value_inv _#6 value_sigma H2); clear H2.
    intros A'' B'' Hal'' Hbl'' Heq2.
    so (eqtrans Heq1 (eqsymm Heq2)) as Heq.
    clear Heq2.
    subst R.
    so (iusigma_inj _#5 Heq) as H; clear Heq.
    injectionT H.
    intros <-.
    injectionT H.
    intros <-.
    so (basic_fun _#7 (basic_downward _#7 Hj Hal) Hal'); subst A'.
    so (functional_fun _#8 (functional_downward _#8 Hj Hbl) Hbl'); subst B'.
    apply (relhyp_tm _#4 (iutruncate (S j) (pi1 B (embed_ceiling _ _ (urelspinj (ceiling (S j) (den A)) _#3 (conj (Nat.lt_succ_diag_r j) (urel_downward_leq _#6 Hj Hpq1))))))).
      {
      invert Hbl'.
      intros B' _ _ Hact Heq.
      so (eq_dep_impl_eq_snd _#5 Heq); subst B'; clear Heq.
      so (Hact _#3 (le_refl _) (conj (Nat.lt_succ_diag_r j) (urel_downward_leq _#6 Hj Hpq1))) as H.
      cbn in H.
      eapply basic_equiv; eauto; clear H; try prove_hygiene.
      simpsub.
      apply equiv_symm.
      apply equiv_funct; auto using equiv_refl.
      apply equivsub_dot; auto using equivsub_refl.
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hstepsp.
        }
      apply star_one; apply step_ppi12.
      }

      {
      invert Hbl''.
      intros B' _ _ Hact Heq.
      so (eq_dep_impl_eq_snd _#5 Heq); subst B'; clear Heq.
      so (Hact _#3 (le_refl _) Hr) as H.
      cbn in H.
      rewrite -> embed_ceiling_urelspinj.
      destruct Hr as (Hj' & Hr).
      rewrite -> embed_ceiling_urelspinj in H.
      simpsubin H.
      force_exact H.
      unfold interp.
      f_equal.
      f_equal; f_equal.
      apply urelspinj_equal.
      refine (urel_equiv_2 _#6 _ _ Hr).
        {
        exact (urel_closed _#5 Hpq1 ander).
        }
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hstepsq.
        }
      apply star_one; apply step_ppi12.
      }
    }
  }

  {
  simpsub.
  apply equivsub_dot; auto using equivsub_refl.
  apply (equiv_trans _ _ (ppair p1 p2)).
    {
    apply equiv_ppair.
      {
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hstepsp.
        }
      apply star_one; apply step_ppi12.
      }

      {
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi2); auto using step_ppi21.
        exact Hstepsp.
        }
      apply star_one; apply step_ppi22.
      }
    }

    {
    apply equiv_symm.
    apply steps_equiv; eauto.
    }
  }

  {
  simpsub.
  apply equivsub_dot; auto using equivsub_refl.
  apply (equiv_trans _ _ (ppair q1 q2)).
    {
    apply equiv_ppair.
      {
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hstepsq.
        }
      apply star_one; apply step_ppi12.
      }

      {
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi2); auto using step_ppi21.
        exact Hstepsq.
        }
      apply star_one; apply step_ppi22.
      }
    }

    {
    apply equiv_symm.
    apply steps_equiv; eauto.
    }
  }

  {
  intros j d uu Hji Huu.
  so (smaller_impl_le _#3 Hji) as Hj.
  rewrite -> !qpromote_cons in Huu.
  rewrite -> !qpromote_hyp_tm in Huu.
  simpsubin Huu.
  invertc Huu.
  intros r2 uu' Huu' Hr2 <-.
  invertc Huu'.
  intros r1 u Hu Hr1 <-.
  simpsub.
  rewrite -> qpromote_cons.
  rewrite -> qpromote_hyp_tm.
  apply seqctx_cons; auto.
  simpsub.
  invertc Hr1.
  intros A' Hal' Har' Hr1.
  so (basic_fun _#7 (basic_downward _#7 Hj Hal) Hal'); subst A'.
  invertc Hr2.
  intros R Hbpl Hbrr Hr2.
  so (urel_closed _#5 Hr1 ander) as Hclr1.
  so (urel_closed _#5 Hr2 ander) as Hclr2.
  so (urel_closed _#5 Hpq1 andel) as Hclp1.
  so (urel_closed _#5 Hpq2 andel) as Hclp2.
  apply (seqhyp_relhyp_2 _#4 (hyp_tm (subst s' (sigma a b)))).
    {
    exploit (Hleft _#3 Hji Hu) as H.
    rewrite -> qpromote_hyp_tm in H.
    simpsubin H.
    simpsub.
    exact H.
    }
  apply (seqhyp_tm _#5 (iutruncate (S j) (iusigma stop A B))).
    {
    exact (basic_downward _#7 Hj Habl).
    }

    {
    simpsub.
    exact (basic_downward _#7 Hj Habr).
    }

    {
    destruct Hr1 as (Hjs & Hr1).
    split; auto.
    assert (rel (den A) j p1 r1) as Hpr1.
      {
      eapply urel_equiv_1; eauto; try prove_hygiene.
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hstepsp.
        }
      apply star_one; apply step_ppi12.
      }
    exists p1, r1, p2, r2, Hpr1.
    do2 4 split; auto using star_refl; try prove_hygiene.
    cbn.
    invert Hbl.
    intros _ _ Hact.
    so (Hact _#3 (le_refl _) Hpq1) as H; clear Hact.
    simpsubin H.
    eassert _; [refine (basic_fun _#7 (basic_equiv _#7 _ _ Hbpl) (basic_downward _#7 Hj H)) |]; clear H; try prove_hygiene.
      {
      apply equiv_funct; auto using equiv_refl.
      apply equivsub_dot; auto using equivsub_refl.
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hstepsp.
        }
      apply star_one; apply step_ppi12.
      }
    subst R.
    destruct Hr2 as (_ & Hr2).
    refine (rel_from_dist _#6 _ (urel_equiv_1 _#6 _ _ Hr2)); auto.
      {
      apply den_nonexpansive.
      apply (pi2 B).
      apply urelspinj_dist_diff; auto.
      }

      {
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi2); auto using step_ppi21.
        exact Hstepsp.
        }
      apply star_one; apply step_ppi22.
      }
    }
  }

  {
  intros j d uu Hji Huu.
  so (smaller_impl_le _#3 Hji) as Hj.
  rewrite -> !qpromote_cons in Huu.
  rewrite -> !qpromote_hyp_tm in Huu.
  simpsubin Huu.
  invertc Huu.
  intros r2 uu' Huu' Hr2 <-.
  invertc Huu'.
  intros r1 u Hu Hr1 <-.
  simpsub.
  rewrite -> qpromote_cons.
  rewrite -> qpromote_hyp_tm.
  apply seqctx_cons; auto.
  simpsub.
  invertc Hr1.
  intros A' Hal' Har' Hr1.
  so (basic_fun _#7 (basic_downward _#7 Hj Har) Har'); subst A'.
  invertc Hr2.
  intros R Hbrl Hbpr Hr2.
  so (urel_closed _#5 Hr1 andel) as Hclr1.
  so (urel_closed _#5 Hr2 andel) as Hclr2.
  so (urel_closed _#5 Hpq1 ander) as Hclq1.
  so (urel_closed _#5 Hpq2 ander) as Hclq2.
  apply (seqhyp_relhyp_1 _#3 (hyp_tm (subst s (sigma a b)))).
    {
    exploit (Hright _#3 Hji Hu) as H.
    rewrite -> qpromote_hyp_tm in H.
    simpsubin H.
    simpsub.
    exact H.
    }
  apply (seqhyp_tm _#5 (iutruncate (S j) (iusigma stop A B))).
    {
    simpsub.
    exact (basic_downward _#7 Hj Habl).
    }

    {
    simpsub.
    exact (basic_downward _#7 Hj Habr).
    }

    {
    destruct Hr1 as (Hjs & Hr1).
    split; auto.
    assert (rel (den A) j r1 q1) as Hrq1.
      {
      eapply urel_equiv_2; eauto; try prove_hygiene.
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hstepsq.
        }
      apply star_one; apply step_ppi12.
      }
    exists r1, q1, r2, q2, Hrq1.
    do2 4 split; auto using star_refl; try prove_hygiene.
    cbn.
    invert Hbr.
    intros _ _ Hact.
    so (Hact _#3 (le_refl _) Hpq1) as H; clear Hact.
    simpsubin H.
    eassert _; [refine (basic_fun _#7 (basic_equiv _#7 _ _ Hbpr) (basic_downward _#7 Hj H)) |]; clear H; try prove_hygiene.
      {
      apply equiv_funct; auto using equiv_refl.
      apply equivsub_dot; auto using equivsub_refl.
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi1); auto using step_ppi11.
        exact Hstepsq.
        }
      apply star_one; apply step_ppi12.
      }
    subst R.
    destruct Hr2 as (_ & Hr2).
    refine (rel_from_dist _#6 _ (urel_equiv_2 _#6 _ _ Hr2)); auto.
      {
      apply den_nonexpansive.
      apply (pi2 B).
      apply urelspinj_dist_diff; auto.
      eapply urel_downward_leq; eauto.
      }

      {
      apply steps_equiv.
      eapply star_trans.
        {
        apply (star_map' _ _ ppi2); auto using step_ppi21.
        exact Hstepsq.
        }
      apply star_one; apply step_ppi22.
      }
    }
  }
Qed.

Lemma sound_sigma_ext :
  forall G a b m n a' a'' b' b'',
    pseq G (deq (ppi1 m) (ppi1 n) a)
    -> pseq G (deq (ppi2 m) (ppi2 n) (subst1 (ppi1 m) b))
    -> pseq (cons (hyp_tm a) G) (deqtype b b)
    -> pseq G (deq m m (sigma a' b'))
    -> pseq G (deq n n (sigma a'' b''))
    -> pseq G (deq m n (sigma a b)).
Proof.
intros G a b m n a' a'' b' b''.
revert G.
refine (seq_pseq 3 [hyp_emp] b [] m [] n 5 [] _ [] _ [_] _ [] _ [] _ _ _); cbn.
intros G Hclb Hclm Hcln Hseq1 Hseq2 Hseqb Hseqm Hseqn.
rewrite -> seq_deq in Hseq1, Hseq2, Hseqm, Hseqn |- *.
rewrite -> seq_eqtype in Hseqb.
intros i s s' Hs.
so (pwctx_impl_closub _#4 Hs) as (Hcls & Hcls').
so (Hseq1 _#3 Hs) as (A & Hal & Har & Hm1 & Hn1 & Hmn1).
exploit (extract_functional toppg i (den A) (subst (under 1 s) b) (subst (under 1 s') b)) as H; eauto using subst_closub_under_permit.
  {
  exact (f_equal den (basic_impl_iutruncate _#6 Hal)).
  }

  {
  intros j r t Hrt.
  so (basic_member_index _#9 Hal Hrt) as Hj.
  assert (pwctx j (dot r s) (dot t s') (cons (hyp_tm a) G)) as Hs'.
    {
    apply pwctx_cons_tm_seq; eauto using pwctx_downward.
      {
      apply (seqhyp_tm _#5 (iutruncate (S j) A)).
        {
        eapply basic_downward; eauto.
        }

        {
        eapply basic_downward; eauto.
        }

        {
        split; auto.
        }
      }

      {
      intros j' u u' Hu.
      so (Hseq1 _#3 Hu) as (Q & Hl & Hr & _).
      eauto.
      }
    }
  so (Hseqb _#3 Hs') as (Q & Hl & Hr & _).
  exists Q.
  simpsub.
  auto.
  }
destruct H as (B & Hbl & Hbr).
so (Hseq2 _#3 Hs) as (Bx & Hbxl & _ & Hm2 & Hn2 & Hmn2).
invert Hbl.
intros _ _ Hact.
so (Hact _ _ _ (le_refl _) Hm1) as Hbxl'; clear Hact.
simpsubin Hbxl.
simpsubin Hbxl'.
so (basic_fun _#7 Hbxl Hbxl'); subst Bx.
clear Hbxl Hbxl'.
so (Hseqm _#3 Hs) as (R & Hsigl & _ & Hm & _).
simpsubin Hsigl.
invert (basic_value_inv _#6 value_sigma Hsigl).
intros A' B' _ _ <-.
cbn in Hm.
decompose Hm.
intros m1 m1' m2 m2' _ _ _ Hstepsm Hstepsm' _.
clear A' B' Hsigl.
so (Hseqn _#3 Hs) as (R & Hsigl & _ & Hn & _).
simpsubin Hsigl.
invert (basic_value_inv _#6 value_sigma Hsigl).
intros A' B' _ _ <-.
cbn in Hn.
decompose Hn.
intros n1 n1' n2 n2' _ _ _ Hstepsn Hstepsn' _.
clear A' B' Hsigl.
so (hygiene_invert_auto _#5 (steps_hygiene _#4 Hstepsm (subst_closub _#4 Hcls Hclm))) as H; cbn in H.
destruct H as (Hclm1 & Hclm2 & _).
so (hygiene_invert_auto _#5 (steps_hygiene _#4 Hstepsm' (subst_closub _#4 Hcls' Hclm))) as H; cbn in H.
destruct H as (Hclm1' & Hclm2' & _).
so (hygiene_invert_auto _#5 (steps_hygiene _#4 Hstepsn (subst_closub _#4 Hcls Hcln))) as H; cbn in H.
destruct H as (Hcln1 & Hcln2 & _).
so (hygiene_invert_auto _#5 (steps_hygiene _#4 Hstepsn' (subst_closub _#4 Hcls' Hcln))) as H; cbn in H.
destruct H as (Hcln1' & Hcln2' & _).
assert (equiv (ppi1 (subst s m)) m1) as Hequivm1.
  {
  simpsub.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi1); eauto using step_ppi11.
    }
  apply star_one.
  apply step_ppi12.
  }
assert (equiv (ppi1 (subst s' m)) m1') as Hequivm1'.
  {
  simpsub.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi1); eauto using step_ppi11.
    }
  apply star_one.
  apply step_ppi12.
  }
assert (equiv (ppi2 (subst s m)) m2) as Hequivm2.
  {
  simpsub.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi2); eauto using step_ppi21.
    }
  apply star_one.
  apply step_ppi22.
  }
assert (equiv (ppi2 (subst s' m)) m2') as Hequivm2'.
  {
  simpsub.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi2); eauto using step_ppi21.
    }
  apply star_one.
  apply step_ppi22.
  }
assert (equiv (ppi1 (subst s n)) n1) as Hequivn1.
  {
  simpsub.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi1); eauto using step_ppi11.
    }
  apply star_one.
  apply step_ppi12.
  }
assert (equiv (ppi1 (subst s' n)) n1') as Hequivn1'.
  {
  simpsub.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi1); eauto using step_ppi11.
    }
  apply star_one.
  apply step_ppi12.
  }
assert (equiv (ppi2 (subst s n)) n2) as Hequivn2.
  {
  simpsub.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi2); eauto using step_ppi21.
    }
  apply star_one.
  apply step_ppi22.
  }
assert (equiv (ppi2 (subst s' n)) n2') as Hequivn2'.
  {
  simpsub.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi2); eauto using step_ppi21.
    }
  apply star_one.
  apply step_ppi22.
  }
exists (iusigma stop A B).
simpsub.
do2 4 split.
  {
  apply interp_eval_refl.
  apply interp_sigma; auto.
  }

  {
  apply interp_eval_refl.
  apply interp_sigma; auto.
  }

  {
  assert (rel (den A) i m1 m1') as Hrel.
    {
    refine (urel_equiv _#7 _ _ _ _ Hm1); auto.
    }
  exists m1, m1', m2, m2', Hrel.
  do2 4 split; eauto using subst_closub.
  cbn.
  eassert _ as H; [refine (urel_equiv _#4 m2 _ m2' _#4 Hm2) |]; auto.
  force_exact H; clear H.
  do 3 f_equal.
  apply urelspinj_equal.
  refine (urel_equiv_2 _#6 _ _ Hm1); auto.
  }

  {
  assert (rel (den A) i n1 n1') as Hrel.
    {
    refine (urel_equiv _#7 _ _ _ _ Hn1); auto.
    }
  exists n1, n1', n2, n2', Hrel.
  do2 4 split; eauto using subst_closub.
  cbn.
  eassert _ as H; [refine (urel_equiv _#4 n2 _ n2' _#4 Hn2) |]; auto.
  force_exact H; clear H.
  do 3 f_equal.
  apply urelspinj_equal.
  refine (urel_equiv_2 _#6 _ _ Hmn1); auto.
  }

  {
  assert (rel (den A) i m1 n1') as Hrel.
    {
    refine (urel_equiv _#7 _ _ _ _ Hmn1); auto.
    }
  exists m1, n1', m2, n2', Hrel.
  do2 4 split; eauto using subst_closub.
  cbn.
  eassert _ as H; [refine (urel_equiv _#4 m2 _ n2' _#4 Hmn2) |]; auto.
  force_exact H; clear H.
  do 3 f_equal.
  apply urelspinj_equal.
  refine (urel_equiv_2 _#6 _ _ Hmn1); auto.
  }
Qed.

Lemma sound_prod_kind_formation :
  forall G lv k k' l l',
    pseq G (deq k k' (kuniv lv))
    -> pseq G (deq l l' (kuniv lv))
    -> pseq G (deq (prod k l) (prod k' l') (kuniv lv)).
Proof.
intros G lv k1 k2 l1 l2.
revert G.
refine (seq_pseq 0 2 [] _ [] _ _ _); cbn.
intros G Hseqk Hseql.
rewrite -> seq_eqkind in Hseqk, Hseql |- *.
intros i s s' Hs.
so (Hseqk _#3 Hs) as (pg & K & A & hl & Hlvl & Hlvr & Hk1lt & Hk1rt & Hk2lt & Hk2rt & Hk1l & Hk1r & Hk2l & Hk2r).
clear Hseqk.
so (Hseql _#3 Hs) as (pg' & L & B & hl' & Hlvl' & _ & Hl1lt & Hl1rt & Hl2lt & Hl2rt & Hl1l & Hl1r & Hl2l & Hl2r).
clear Hseql.
so (pginterp_fun _#3 Hlvl Hlvl'); subst pg'.
so (proof_irrelevance _ hl hl'); subst hl'.
exists pg, (qprod K L), (iuprod stop A B), hl.
simpsub.
do2 9 split; auto;
try (apply kinterp_eval_refl; apply interp_kprod; auto; done);
apply interp_eval_refl; apply interp_prod; auto.
Qed.

Lemma sound_prod_formation :
  forall G k k' l l',
    pseq G (deqtype k k')
    -> pseq G (deqtype l l')
    -> pseq G (deqtype (prod k l) (prod k' l')).
Proof.
intros G k1 k2 l1 l2.
revert G.
refine (seq_pseq 0 2 [] _ [] _ _ _); cbn.
intros G Hseqk Hseql.
rewrite -> seq_eqtype in Hseqk, Hseql |- *.
intros i s s' Hs.
so (Hseqk _#3 Hs) as (A & Hk1l & Hk1r & Hk2l & Hk2r).
so (Hseql _#3 Hs) as (B & Hl1l & Hl1r & Hl2l & Hl2r).
clear Hseqk Hseql.
exists (iuprod stop A B).
simpsub.
do2 3 split; auto;
apply interp_eval_refl;
apply interp_prod; auto.
Qed.

Lemma sound_prod_formation_univ :
  forall G lv k k' l l',
    pseq G (deq k k' (univ lv))
    -> pseq G (deq l l' (univ lv))
    -> pseq G (deq (prod k l) (prod k' l') (univ lv)).
Proof.
intros G lv k1 k2 l1 l2.
revert G.
refine (seq_pseq 0 2 [] _ [] _ _ _); cbn.
intros G Hseqk Hseql.
rewrite -> seq_univ in Hseqk, Hseql |- *.
intros i s s' Hs.
so (Hseqk _#3 Hs) as (pg & A & Hlvl & Hlvr & Hk1l & Hk1r & Hk2l & Hk2r).
so (Hseql _#3 Hs) as (pg' & B & Hlvl' & _ & Hl1l & Hl1r & Hl2l & Hl2r).
clear Hseqk Hseql.
so (pginterp_fun _#3 Hlvl Hlvl'); subst pg'.
exists pg, (iuprod stop A B).
simpsub.
do2 5 split; auto;
apply interp_eval_refl;
apply interp_prod; auto.
Qed.

Lemma sound_prod_sigma_equal :
  forall G a b,
    pseq G (deqtype a a)
    -> pseq G (deqtype b b)
    -> pseq G (deqtype (prod a b) (sigma a (subst sh1 b))).
Proof.
intros G a b.
revert G.
refine (seq_pseq 1 [] b 2 [] _ [] _ _ _); cbn.
intros G Hclb Hseqa Hseqb.
rewrite -> seq_eqtype in Hseqa, Hseqb |- *.
intros i s s' Hs.
so (pwctx_impl_closub _#4 Hs) as (Hcls & Hcls').
so (Hseqa _#3 Hs) as (A & Hal & Har & _).
so (Hseqb _#3 Hs) as (B & Hbl & Hbr & _).
exists (iuprod stop A B).
simpsub.
assert (den A = ceiling (S i) (den A)) as HeqA.
  {
  so (basic_impl_iutruncate _#6 Hal) as Heq.
  exact (f_equal den Heq).
  }
do2 3 split; auto;
apply interp_eval_refl;
try (apply interp_prod); auto.
  {
  rewrite -> iuprod_eq_iusigma.
  apply interp_sigma; auto.
  apply functional_i; auto.
    {
    rewrite -> subst_compose.
    apply hygiene_shift_permit.
    eapply subst_closub; eauto.
    }
  intros j m p Hj Hmp.
  cbn.
  unfold semiconst.
  rewrite -> urelsp_index_inj.
  simpsub.
  eapply basic_downward; eauto.
  }

  {
  rewrite -> iuprod_eq_iusigma.
  apply interp_sigma; auto.
  apply functional_i; auto.
    {
    rewrite -> subst_compose.
    apply hygiene_shift_permit.
    eapply subst_closub; eauto.
    }
  intros j m p Hj Hmp.
  cbn.
  unfold semiconst.
  rewrite -> urelsp_index_inj.
  simpsub.
  eapply basic_downward; eauto.
  }
Qed.

Lemma sound_prod_sigma_equal_univ :
  forall G lv a b,
    pseq G (deq a a (univ lv))
    -> pseq G (deq b b (univ lv))
    -> pseq G (deq (prod a b) (sigma a (subst sh1 b)) (univ lv)).
Proof.
intros G lv a b.
revert G.
refine (seq_pseq 1 [] b 2 [] _ [] _ _ _); cbn.
intros G Hclb Hseqa Hseqb.
rewrite -> seq_univ in Hseqa, Hseqb |- *.
intros i s s' Hs.
so (pwctx_impl_closub _#4 Hs) as (Hcls & Hcls').
so (Hseqa _#3 Hs) as (pg & A & Hlvl & Hlvr & Hal & Har & _).
so (Hseqb _#3 Hs) as (pg' & B & Hlvl' & _ & Hbl & Hbr & _).
so (pginterp_fun _#3 Hlvl Hlvl'); subst pg'.
exists pg, (iuprod stop A B).
simpsub.
assert (den A = ceiling (S i) (den A)) as HeqA.
  {
  so (basic_impl_iutruncate _#6 Hal) as Heq.
  exact (f_equal den Heq).
  }
do2 5 split; auto;
apply interp_eval_refl;
try (apply interp_prod); auto.
  {
  rewrite -> iuprod_eq_iusigma.
  apply interp_sigma; auto.
  apply functional_i; auto.
    {
    rewrite -> subst_compose.
    apply hygiene_shift_permit.
    eapply subst_closub; eauto.
    }
  intros j m p Hj Hmp.
  cbn.
  unfold semiconst.
  rewrite -> urelsp_index_inj.
  simpsub.
  eapply basic_downward; eauto.
  }

  {
  rewrite -> iuprod_eq_iusigma.
  apply interp_sigma; auto.
  apply functional_i; auto.
    {
    rewrite -> subst_compose.
    apply hygiene_shift_permit.
    eapply subst_closub; eauto.
    }
  intros j m p Hj Hmp.
  cbn.
  unfold semiconst.
  rewrite -> urelsp_index_inj.
  simpsub.
  eapply basic_downward; eauto.
  }
Qed.

Lemma sound_prod_elim1 :
  forall G a b m n,
    pseq G (deq m n (prod a b))
    -> pseq G (deq (ppi1 m) (ppi1 n) a).
Proof.
intros G a b m n.
revert G.
refine (seq_pseq 0 1 [] _ _ _); cbn.
intros G Hseq.
rewrite -> seq_deq in Hseq |- *.
intros i s s' Hs.
so (Hseq _#3 Hs) as (R & Hl & Hr & Hm & Hn & Hmn).
simpsubin Hl.
simpsubin Hr.
invert (basic_value_inv _#6 value_prod Hl).
intros A B Hal Hbl Heq1.
invert (basic_value_inv _#6 value_prod Hr).
intros A' B' Har Hbr Heq2.
so (eqtrans Heq1 (eqsymm Heq2)) as Heq.
clear Heq2.
subst R.
so (iuprod_inj _#5 Heq) as (<- & _); clear Heq.
exists A.
do2 2 split; auto.
simpsub.
clear Hseq.
revert m n Hm Hn Hmn.
cut (forall m n,
       rel (den (iuprod stop A B)) i m n
       -> rel (den A) i (ppi1 m) (ppi1 n)).
  {
  intros.
  do2 2 split; auto.
  }
intros m n Hmn.
cbn in Hmn.
decompose Hmn.
intros m1 n1 m2 n2 Hclm Hcln Hstepsm Hstepsn Hmn1 Hmn2.
refine (urel_equiv _#7 _ _ _ _ Hmn1); try prove_hygiene.
  {
  apply equiv_symm.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi1); auto using step_ppi11.
    exact Hstepsm.
    }
  apply star_one; apply step_ppi12.
  }

  {
  apply equiv_symm.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi1); auto using step_ppi11.
    exact Hstepsn.
    }
  apply star_one; apply step_ppi12.
  }
Qed.

Lemma sound_prod_elim2 :
  forall G a b m n,
    pseq G (deq m n (prod a b))
    -> pseq G (deq (ppi2 m) (ppi2 n) b).
Proof.
intros G a b m n.
revert G.
refine (seq_pseq 0 1 [] _ _ _); cbn.
intros G Hseq.
rewrite -> seq_deq in Hseq |- *.
intros i s s' Hs.
so (Hseq _#3 Hs) as (R & Hl & Hr & Hm & Hn & Hmn).
simpsubin Hl.
simpsubin Hr.
invert (basic_value_inv _#6 value_prod Hl).
intros A B Hal Hbl Heq1.
invert (basic_value_inv _#6 value_prod Hr).
intros A' B' Har Hbr Heq2.
so (eqtrans Heq1 (eqsymm Heq2)) as Heq.
clear Heq2.
subst R.
so (iuprod_inj _#5 Heq) as (<- & Heq'); clear Heq.
assert (B = B').
  {
  cbn in Hm.
  decompose Hm.
  intros p q _ _ _ _ _ _ H _.
  so (Heq' _#3 H) as Heq.
  rewrite <- (basic_impl_iutruncate _#6 Hbl) in Heq.
  rewrite <- (basic_impl_iutruncate _#6 Hbr) in Heq.
  exact Heq.
  }
subst B'.
clear Heq'.
exists B.
do2 2 split; auto.
simpsub.
clear Hseq.
revert m n Hm Hn Hmn.
cut (forall m n,
       rel (den (iuprod stop A B)) i m n
       -> rel (den B) i (ppi2 m) (ppi2 n)).
  {
  intros.
  do2 2 split; auto.
  }
intros m n Hmn.
cbn in Hmn.
decompose Hmn.
intros m1 n1 m2 n2 Hclm Hcln Hstepsm Hstepsn Hmn1 Hmn2.
refine (urel_equiv _#7 _ _ _ _ Hmn2); try prove_hygiene.
  {
  apply equiv_symm.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi2); auto using step_ppi21.
    exact Hstepsm.
    }
  apply star_one; apply step_ppi22.
  }

  {
  apply equiv_symm.
  apply steps_equiv.
  eapply star_trans.
    {
    apply (star_map' _ _ ppi2); auto using step_ppi21.
    exact Hstepsn.
    }
  apply star_one; apply step_ppi22.
  }
Qed.

Lemma sound_sigma_formation_invert1 :
  forall G a a' b b',
    pseq G (deqtype (sigma a b) (sigma a' b'))
    -> pseq G (deqtype a a').
Proof.
intros G a b c d.
revert G.
refine (seq_pseq 0 1 [] _ _ _); cbn.
intros G Hseq.
rewrite -> seq_eqtype in Hseq |- *.
intros i s s' Hs.
so (Hseq _#3 Hs) as (R & Hpil & Hpir & Hpil' & Hpir').
simpsubin Hpil.
simpsubin Hpir.
simpsubin Hpil'.
simpsubin Hpir'.
invert (basic_value_inv _#6 value_sigma Hpil).
intros A B Hal Hbl Heql.
invert (basic_value_inv _#6 value_sigma Hpir).
intros A' B' Har Hbr Heqr.
so (iusigma_inj _#5 (eqtrans Heql (eqsymm Heqr))) as H.
injectionT H.
intros <-.
injectionT H.
intros <-.
invert (basic_value_inv _#6 value_sigma Hpil').
intros A' B' Hal' Hbl' Heql'.
so (iusigma_inj _#5 (eqtrans Heql (eqsymm Heql'))) as H.
injectionT H.
intros <-.
injectionT H.
intros <-.
invert (basic_value_inv _#6 value_sigma Hpir').
intros A' B' Har' Hbr' Heqr'.
so (iusigma_inj _#5 (eqtrans Heql (eqsymm Heqr'))) as H.
injectionT H.
intros <-.
injectionT H.
intros <-.
exists A.
auto.
Qed.

Lemma sound_sigma_formation_invert2 :
  forall G a a' b b',
    pseq G (deqtype (sigma a b) (sigma a' b'))
    -> pseq (cons (hyp_tm a) G) (deqtype b b').
Proof.
intros G a b c d.
revert G.
refine (seq_pseq_hyp 4 [] a [] b [hyp_emp] c [hyp_emp] d 1 [] [] _ [] [_] _ _); cbn.
intros G Hcla Hclb Hclc Hcld Hseq _.
rewrite -> seq_eqtype in Hseq |- *.
intros i ss ss' Hss.
so (pwctx_cons_invert_simple _#5 Hss) as H; clear Hss.
destruct H as (m & p & s & s' & Hs & Hmp & -> & ->).
so (Hseq i s s' Hs) as (R & Hpil & Hpir & Hpil' & Hpir').
simpsubin Hpil.
simpsubin Hpir.
simpsubin Hpil'.
simpsubin Hpir'.
invert (basic_value_inv _#6 value_sigma Hpil).
intros A B Hal Hcl Heqacl.
invert (basic_value_inv _#6 value_sigma Hpir).
intros A' B' Har Hcr Heqacr.
so (eqtrans Heqacl (eqsymm Heqacr)) as Heq.
clear Heqacr.
invert (basic_value_inv _#6 value_sigma Hpil').
intros A'' B'' Hbl Hdl Heqbdl.
so (eqtrans Heqacl (eqsymm Heqbdl)) as Heq'.
clear Heqbdl.
invert (basic_value_inv _#6 value_sigma Hpir').
intros A''' B''' Hbr Hdr Heqbdr.
so (eqtrans Heqacl (eqsymm Heqbdr)) as Heq''.
clear Heqbdr.
subst R.
so (iusigma_inj _#5 Heq) as H.
injectionT H.
intros <-.
injectionT H.
intros <-.
so (iusigma_inj _#5 Heq') as H.
injectionT H.
intros <-.
injectionT H.
intros <-.
so (iusigma_inj _#5 Heq'') as H.
injectionT H.
intros <-.
injectionT H.
intros <-.
clear Heq Heq' Heq''.
invertc Hmp.
intros A' Hal' _ Hmp.
so (basic_fun _#7 (interp_increase _#6 (toppg_max _) Hal) Hal'); subst A'.
exists (pi1 B (urelspinj (den A) i m p Hmp)).
simpsub.
do2 3 split.
  {
  invert Hcl.
  intros _ _ Hact.
  so (Hact _#3 (le_refl _) Hmp) as H.
  simpsubin H.
  exact H.
  }

  {
  invert Hcr.
  intros _ _ Hact.
  so (Hact _#3 (le_refl _) Hmp) as H.
  simpsubin H.
  exact H.
  }

  {
  invert Hdl.
  intros _ _ Hact.
  so (Hact _#3 (le_refl _) Hmp) as H.
  simpsubin H.
  exact H.
  }

  {
  invert Hdr.
  intros _ _ Hact.
  so (Hact _#3 (le_refl _) Hmp) as H.
  simpsubin H.
  exact H.
  }
Qed.

Lemma sound_prod_formation_invert1 :
  forall G a a' b b',
    pseq G (deqtype (prod a b) (prod a' b'))
    -> pseq G (deqtype a a').
Proof.
intros G a b c d.
revert G.
refine (seq_pseq 0 1 [] _ _ _); cbn.
intros G Hseq.
rewrite -> seq_eqtype in Hseq |- *.
intros i s s' Hs.
so (Hseq _#3 Hs) as (R & Hpil & Hpir & Hpil' & Hpir').
simpsubin Hpil.
simpsubin Hpir.
simpsubin Hpil'.
simpsubin Hpir'.
invert (basic_value_inv _#6 value_prod Hpil).
intros A B Hal Hbl Heql.
invert (basic_value_inv _#6 value_prod Hpir).
intros A' B' Har Hbr Heqr.
so (iuprod_inj _#5 (eqtrans Heql (eqsymm Heqr))) as (<- & _).
invert (basic_value_inv _#6 value_prod Hpil').
intros A' B'' Hal' Hbl' Heql'.
so (iuprod_inj _#5 (eqtrans Heql (eqsymm Heql'))) as (<- & _).
invert (basic_value_inv _#6 value_prod Hpir').
intros A' B''' Har' Hbr' Heqr'.
so (iuprod_inj _#5 (eqtrans Heql (eqsymm Heqr'))) as (<- & _).
exists A.
auto.
Qed.

Lemma sound_prod_formation_invert2 :
  forall G a a' b b',
    pseq G (deqtype (prod a b) (prod a' b'))
    -> pseq (cons (hyp_tm a) G) (deqtype (subst sh1 b) (subst sh1 b')).
Proof.
intros G a b c d.
revert G.
refine (seq_pseq_hyp 4 [] a [] b [] c [] d 1 [] [] _ [] [_] _ _); cbn.
intros G Hcla Hclb Hclc Hcld Hseq _.
rewrite -> seq_eqtype in Hseq |- *.
intros i ss ss' Hss.
so (pwctx_cons_invert_simple _#5 Hss) as H; clear Hss.
destruct H as (m & p & s & s' & Hs & Hmp & -> & ->).
simpsubin Hmp.
invertc Hmp.
intros A Hal Har Hmp.
so (Hseq i s s' Hs) as (R & Hpil & Hpir & Hpil' & Hpir').
simpsubin Hpil.
simpsubin Hpir.
simpsubin Hpil'.
simpsubin Hpir'.
invert (basic_value_inv _#6 value_prod Hpil).
intros A' B Hal' Hcl Heqacl.
so (basic_fun _#7 Hal Hal'); subst A'.
invert (basic_value_inv _#6 value_prod Hpir).
intros A' B' Har' Hcr Heqacr.
so (eqtrans Heqacl (eqsymm Heqacr)) as Heq.
clear Heqacr.
invert (basic_value_inv _#6 value_prod Hpil').
intros A'' B'' Hbl Hdl Heqbdl.
so (eqtrans Heqacl (eqsymm Heqbdl)) as Heq'.
clear Heqbdl.
invert (basic_value_inv _#6 value_prod Hpir').
intros A''' B''' Hbr Hdr Heqbdr.
so (eqtrans Heqacl (eqsymm Heqbdr)) as Heq''.
clear Heqbdr.
subst R.
so (iuprod_inj _#5 Heq) as (<- & H).
so (H _#3 Hmp) as HeqB; clear H.
rewrite <- (basic_impl_iutruncate _#6 Hcl) in HeqB.
rewrite <- (basic_impl_iutruncate _#6 Hcr) in HeqB.
subst B'.
so (iuprod_inj _#5 Heq') as (<- & H).
so (H _#3 Hmp) as HeqB; clear H.
rewrite <- (basic_impl_iutruncate _#6 Hcl) in HeqB.
rewrite <- (basic_impl_iutruncate _#6 Hdl) in HeqB.
subst B''.
so (iuprod_inj _#5 Heq'') as (<- & H).
so (H _#3 Hmp) as HeqB; clear H.
rewrite <- (basic_impl_iutruncate _#6 Hcl) in HeqB.
rewrite <- (basic_impl_iutruncate _#6 Hdr) in HeqB.
subst B'''.
exists B.
simpsub.
do2 3 split; auto.
Qed.

author: kcrary

repo: istari

save_path: github-repos/coq/kcrary-istari


text:
(*
WreckIt Ralph

████████████████████████████████
██████▓▓▓▓█████▓▓▓▓████▓▓▓▓█████
████████▓▓▓▓▓▓▓▓▓▓▓██▓▓▓▓███████
███▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓███
█████▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓█████
█▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓█
███▓▓▓▓▓▓▓▓░░░░░░░░░░▓▓▓▓▓▓▓▓███
█████▓▓▓▓▒▒██░░░░░░██▒▒▓▓▓▓█████
███▓▓▓▓▓▓▒▒▒▒██▓▓██▒▒▒▒▓▓▓▓▓▓███
█▓▓▒▒▒▒▓▓▒▒────▒▒────▒▒▓▓▒▒▒▒▓▓█
███░░▒▒▓▓░░──██░▒██──░░▓▓▒▒░░███
███░░░░▓▓░░░░▓▓▓▓▓▓░░░░▓▓░░░░███
███████░░░░░░▓▓▓▓▓▓░░░░░░███████
███████░░░░░░░░░░░░░░░░░░███████
█████░░░░██▀▀▀▀▀▀▀▀▀▀██░░░░█████
█████░░████▄▄▄▄▄▄▄▄▄▄████░░█████
█████░░██████████████████░░█████
█████░░██▒▒██▓▓▓▓▓▓██▒▒██░░█████
█████░░██▓█▀▀▀▀▀▀▀▀▀▀█▓██░░█████
█████░░████▄▄▄▄▄▄▄▄▄▄████░░█████
███████░░░░░░░░░░░░░░░░░░███████
█████████▒▒▒▒▒▒▒▒▒▒▒▒▒▒█████████
████████████████████████████████

"I'm Gonna Wreck It!"

wreckit is a tactic to break down:
  - exists in hypotheses
  - conjuction in hypotheses
  - disjunction in hypotheses
  - conjuction in the goal
  - constructors in the goal that solve the goal.
  - inductive predicates that when inverted do not create more goals.
*)

Require Import CoqStock.TacticState.

(* wreck_exists:
  - finds an exists in the hypotheses
  - inverts that hypothesis
  - removes that hypothesis and
  - substitutes all variables
  ```
  H: exists x : ?X, ?Y
  ->
  x: ?X
  H: ?Y
  ```
*)
Ltac wreck_exists H :=
  match type of H with
  | exists E, _ = _ =>
    destruct H as [E H];
    try rewrite H in *;
    try wreck_exists H
  | exists E, _ =>
    destruct H as [E H];
    try wreck_exists H
  end.

Tactic Notation "wreck_exists" "in" hyp(H) :=
  wreck_exists H.

Tactic Notation "wreck_exists" "in" "*" :=
  match goal with
  | [ H: exists _, _ = _ |- _ ] =>
    wreck_exists in H
  | [ H: exists _, _ |- _ ] =>
    wreck_exists in H
  end.

Example example_wreck_exists: forall (x: nat) (e: exists (y: nat) (z: nat), x = S y /\ y = O),
  x = S O.
Proof.
intros.
wreck_exists in e.
inversion_clear e.
subst.
reflexivity.
Qed.

Example example_wreck_exists_neq: forall (x: nat) (e: exists (y: nat), x = S y),
  x <> O.
Proof.
intros.
wreck_exists in *.
discriminate.
Qed.

(* wreck_conj:
  - finds a conjunction in the hypotheses
  - inverts that hypothesis
  - clears that hypothesis
  - substitutes all variables
  ```
  H: ?X /\ ?Y ->
  H_left: ?X
  H_right: ?Y
  ```
*)
Ltac wreck_conj H :=
  match type of H with
  | _ /\ _ =>
    let L := fresh H in
    destruct H as [L H];
    try rewrite L in *;
    try rewrite H in *;
    try wreck_conj H
  end.

Tactic Notation "wreck_conj" "in" hyp(H) :=
  wreck_conj H.

Tactic Notation "wreck_conj" "in" "*" :=
  match goal with
  | [ H: _ /\ _ |- _ ] =>
    wreck_conj in H
  end.

Example example_wreck_conj: forall (x: nat) (e: exists (y: nat), x = S y /\ y = O),
  x = S O.
Proof.
intros.
wreck_exists in *.
wreck_conj in e.
reflexivity.
Qed.

Example example_wreck_conj2: forall (P Q R :Prop),
  P /\ Q /\ R -> R.
Proof.
intros.
wreck_conj in H.
assumption.
Qed.

Ltac wreck_conj_as H I :=
  match type of H with
  | _ /\ _ =>
    destruct H as I
  end.

Tactic Notation "wreck_conj" "in" hyp(H) "as" simple_intropattern(I) :=
  wreck_conj_as H I.

Example example_wreck_conj2_as: forall (P Q R :Prop),
  P /\ Q /\ R -> R.
Proof.
intros.
wreck_conj in H as [Hone [Htwo Hthree]].
assumption.
Qed.

(* wreck_disj:
  - finds a disjunction in the hypotheses
  - inverts that hypothesis
  - clears that hypothesis
  ```
  H: ?X \/ ?Y ->
     2 goals
     - H1: ?X
     - H2: ?Y
  ```
*)
Ltac wreck_disj H :=
  match type of H with
  | _ \/ _ =>
    let L := fresh H
    in destruct H as [H | H];
    try rewrite H in *;
    try wreck_disj H
  end.

Tactic Notation "wreck_disj" "in" hyp(H) :=
  wreck_disj H.

Tactic Notation "wreck_disj" "in" "*" :=
  match goal with
  | [ H: _ \/ _ |- _ ] =>
    wreck_disj in H
  end.

Example example_wreck_disj: forall (x: nat) (p: x = 0 \/ x = 1),
  x < 2.
Proof.
intros.
wreck_disj in p.
- auto.
- auto.
Qed.

Example example_wreck_disj2: forall (x: nat) (p: x = 0 \/ x = 1 \/ x = 2),
  x < 3.
Proof.
intros.
wreck_disj in p.
- auto.
- auto.
- auto.
Qed.

Ltac wreck_disj_as H I :=
  match type of H with
  | _ \/ _ =>
    destruct H as I
  end.

Tactic Notation "wreck_disj" "in" hyp(H) "as" simple_intropattern(I) :=
  wreck_disj_as H I.

Example example_wreck_disj2_as: forall (x: nat) (p: x = 0 \/ x = 1 \/ x = 2),
  x < 3.
Proof.
intros.
wreck_disj in p as [p | [p | p]].
- subst. auto.
- subst. auto.
- subst. auto.
Qed.

Local Theorem conj2: forall (P: Prop),
  P -> P /\ P.
Proof.
intros.
constructor; assumption.
Qed.

(* constructor_conj
   If the goal is a conjuction,
   then deconstruct it into two goals.
   ```
   ?X /\ ?Y ->
   2 goals
   - ?X
   - ?Y
   ```
   or one goal if possible
   ```
   ?X /\ ?X -> ?X
   ```
*)
Ltac constructor_conj :=
  match goal with
  | [ |- ?X /\ ?X ] =>
    apply conj2
  | [ |- _ /\ _ ] =>
    apply conj
  end.

Example example_constructor_conj: forall (x: nat) (p: x = 0),
  x < 2 /\ x < 3.
Proof.
intros.
constructor_conj.
- rewrite p.
  auto.
- rewrite p.
  auto.
Qed.

Example example_duplicate_conj: forall (x: nat) (p: x = 0),
  x < 2 /\ x < 2.
Proof.
intros.
constructor_conj.
rewrite p.
auto.
Qed.

(* constructor_zero
   apply constructor only if it solves the goal
*)
Ltac constructor_zero :=
  constructor; fail.

Example example_constructor_zero:
  True -> True.
Proof.
intros.
constructor_zero.
Qed.

Example example_constructor_zero_fail:
  True -> True /\ True.
Proof.
intros.
Fail constructor_zero.
Abort.

(* wreck_one
   If the goal is an inductive predicate,
   then deconstruct it only if it does not create extra goals.
   ```
   H: ?X /\ ?Y ->
   H0: ?X
   H1: ?Y
   ```
   or given the following inductive type,
   which simply boxes a type:
   ```
   Inductive box (T: Type) :=
    | mk_box: T -> box T.
   ```
   inverts the box:
   ```
   box False ->
   False
   ```
*)
Ltac wreck_one H :=
  tryif has_state H
  then
    fail
  else
    (
      (* inversion completes the proof *)
      inversion H; fail
    ) || (
      (* inversion doesn't create an extra goal *)
      let Hi := fresh H in
      inversion H as [Hi];
      add_state H;
      try wreck_one Hi
    ).
(* TODO: Help Wanted
   Question:
     We found that `tryif has_state H then fail` is necessary,
     but we would think that `has_state H ||` would have worked.
     Why is tryif necessary in this case?
*)

Tactic Notation "wreck_one" "in" hyp(H) :=
  wreck_one H.

Tactic Notation "wreck_one" "in" "*" :=
  match goal with
  | [ H: _ |- _ ] =>
    wreck_one H
  end.

Inductive example_type_for_inversion (T: Type) :=
  | example_constructor: T -> example_type_for_inversion T.

Example example_invert_one:
  example_type_for_inversion (example_type_for_inversion (2 = 3)) -> False.
Proof.
intros.
wreck_one in H.
Qed.

Example example_invert_one_conj:
  forall (P Q : Prop),
    (P /\ Q) -> P.
Proof.
  intros.
  wreck_one in H.
  assumption.
Qed.

Example example_invert_zero:
  forall (P: Prop),
    False -> P.
Proof.
  intros.
  wreck_one in H.
Qed.

Example example_invert_one_disj_fail:
  forall (P Q : Prop),
    (P \/ Q) -> Q \/ P.
Proof.
  intros.
  Fail wreck_one in H.
Abort.

Example example_invert_one_noop_because_two_goals:
  forall (P Q : Prop),
    (P \/ Q) -> Q \/ P.
Proof.
  intros.
  Fail wreck_one in H.
Abort.

Example example_invert_one_multiple_hypotheses:
  forall (P Q R : Prop),
    (P /\ Q) -> P /\ R -> P.
Proof.
  intros.
  wreck_one in *.
  wreck_one in *.
  has_state H0.
  Fail wreck_one.
  assumption.
Qed.

Ltac wreck_one_as H I :=
  inversion H as I.

Tactic Notation "wreck_one" "in" hyp(H) "as" simple_intropattern(I) :=
  wreck_one_as H I.

Example example_wreck_one_as:
  forall (P Q : Prop),
    (P /\ Q) -> P.
Proof.
  intros.
  wreck_one in H as [H1 H2].
  exact H1.
Qed.

(* wreckit_step is helpful for seeing what wreckit does step by step *)
Ltac wreckit_step :=
     wreck_exists in *
  || wreck_conj in *
  || wreck_disj in *
  || constructor_conj
  || constructor_zero
  || wreck_one in *
  .

Ltac wreckit := repeat wreckit_step ; clear_states.

Tactic Notation "wreckit" "in" hyp(H) :=
     wreck_exists in H
  || wreck_conj in H
  || wreck_disj in H
  || wreck_one in H
  .

Example example_wreckit: forall (x: nat) (e: exists (y: nat), x = S y /\ y = O),
  x = S O /\ S O = x.
Proof.
intros.
wreckit; reflexivity.
Qed.

(* This example resulted in endless loop in previous version of wreck_one *)
Example example_one_is_one:
  forall (x: nat), x = 1 -> 1 = 1.
Proof.
intros.
wreckit; auto.
Qed.

Example example_wreckit_disj: forall (x: nat) (e: exists (y: nat), (x = S y \/ S y = x) /\ y = O),
  x = S O \/ S O = x.
Proof.
intros.
wreckit; auto.
Qed.

Example example_wreckit_inversion: example_type_for_inversion (example_type_for_inversion (2 = 3)) -> False.
Proof.
  intros.
  wreckit in H.
Qed.

Tactic Notation "wreckit" "in" hyp(H) "as" simple_intropattern(I) :=
     wreck_conj in H as I
  || wreck_disj in H as I
  || wreck_one in H as I
  .

Example example_wreckit_as: example_type_for_inversion (example_type_for_inversion (2 = 3)) -> False.
Proof.
  intros.
  wreckit in H as [H1].
  wreckit in H1 as [H2].
  discriminate.
Qed.

author: awalterschulze

repo: regex-reexamined-coq


text:
Require Import VST.floyd.proofauto.
Require Import mc_reify.bool_funcs.
Require Import Coq.Logic.JMeq.
Local Open Scope logic.

Require Export mc_reify.reify.
Require Import mc_reify.set_reif.
Require Import MirrorCore.Lemma.
Require Import MirrorCharge.RTac.ReifyLemma.
Require Import mc_reify.update_tycon.
Require Export MirrorCore.RTac.Repeat.
Require Import MirrorCore.RTac.Then.
Require Export MirrorCore.RTac.Try.
Require Export MirrorCore.RTac.First.
Require Import MirrorCore.RTac.Fail.
Require Import MirrorCore.RTac.Simplify.
Require Import MirrorCore.Lambda.RedAll.
Require Import MirrorCore.Lambda.ExprUnify_simul.
Require Import MirrorCore.RTac.RTac.
Require Import MirrorCharge.RTac.Instantiate.
Require Import MirrorCharge.RTac.Intro.
Require Import MirrorCharge.RTac.Apply.
Require Import MirrorCharge.RTac.EApply.
Require Export mc_reify.funcs.
Require Import mc_reify.types.
Require Export mc_reify.reflexivity_tacs.
Require Import mc_reify.get_set_reif.
Require Import mc_reify.func_defs.
Require Import mc_reify.typ_eq.
Require Import mc_reify.func_defs.
Require Import mc_reify.rtac_base.

Lemma semax_set_localD:
    forall temp var ret gt
      id (e: Clight.expr) ty gs P T1 T2 R Post v,
  forall {Espec: OracleKind},
      typeof_temp (mk_tycontext temp var ret gt gs) id = Some ty ->
      is_neutral_cast (implicit_deref (typeof e)) ty = true ->
      msubst_eval_LR T1 T2 e RRRR = Some v ->
      tc_expr_b_norho (mk_tycontext temp var ret gt gs) e = true ->
      assertD P (localD (PTree.set id v T1) T2) R = Post ->
      semax (mk_tycontext temp var ret gt gs) (|> (assertD P (localD T1 T2) R))
        (Sset id e)
          (normal_ret_assert Post).
Proof.
  intros.
  subst Post.
  eapply semax_PTree_set; eauto.
  intro rho.
  apply tc_expr_b_sound with (rho := rho) in H2.
  normalize.
Qed.

Definition set_lemma (temp : PTree.t (type * bool)) (var : PTree.t type)
         (ret : type) (gt : PTree.t type) (id : ident)
         (e : Clight.expr) (ty : type): my_lemma.
reify_lemma reify_vst (semax_set_localD temp var ret gt id e ty).
Defined.

Lemma tc_LR_b_sound: forall Delta P T1 T2 R e1 lr p,
  msubst_eval_LR T1 T2 e1 lr = Some p ->
  assertD P (localD T1 T2) R |-- !! (isptr p) ->
  tc_LR_b_norho Delta e1 lr = true ->
  assertD P (localD T1 T2) R |-- local (tc_LR Delta e1 lr).
Proof.
  intros.
  pose proof msubst_eval_LR_eq P T1 T2 nil (map liftx R) e1 p _ H.
  change (PROPx P (LOCALx (LocalD T1 T2 []) (SEPx (map liftx R)))) with
    (assertD P (localD T1 T2) R) in H2.
  destruct lr; simpl tc_LR in *; simpl tc_LR_b_norho in *; simpl eval_LR in *.
  + rewrite (add_andp _ _ H2).
    rewrite (add_andp _ _ H0).
    rewrite andp_assoc.
    apply andp_left2.
    unfold local, lift1; intro rho; normalize.
    apply tc_lvalue_b'_sound; auto.
  + rewrite (add_andp _ _ H2).
    apply andp_left2.
    unfold local, lift1; intro rho; normalize.
    apply tc_expr_b_sound; auto.
Qed.

Lemma nth_error_prop:
  forall P T1 T2 R Rn (n : nat) S,
  assertD P (localD T1 T2) [Rn] |-- !! S ->
  nth_error R n = Some Rn ->
  assertD P (localD T1 T2) R |-- !! S.
Proof.
  intros.
  unfold assertD in *.
  unfold map in H.
  eapply derives_trans.
  + eapply nth_error_SEP_sepcon_TT with (n := n); [exact H |].
    apply map_nth_error, H0.
  + unfold TT.
    intro rho.
    simpl.
    rewrite @sepcon_prop_prop.
    normalize.
Qed.

Lemma semax_load_localD:
forall (temp : PTree.t (type * bool)) (var : PTree.t type)
     (ret : type) (gt : PTree.t type) (id : ident) (t t_root : type) (e0 e1 : Clight.expr)
     (efs : list efield) (tts : list type)
     (e : type_id_env) (lr : LLRR) (n: nat)
     (gs : PTree.t funspec) (sh : Share.t)
     (P : list Prop) (T1 : PTree.t val) (T2 : PTree.t (type * val))
     (R : list mpred) (Post : environ -> mpred)
     (gfs : list gfield)
     (p p' v : val) (v' : reptype t_root)
     (Espec : OracleKind),
  typeof_temp (mk_tycontext temp var ret gt gs) id = Some t ->
  is_neutral_cast (typeof e0) t = true ->
  msubst_efield_denote T1 T2 efs = Some gfs ->
  legal_nested_efield e t_root e1 gfs tts lr = true ->
  tc_efield_b_norho (mk_tycontext temp var ret gt gs) efs = true ->

  msubst_eval_LR T1 T2 e1 lr = Some p ->
  tc_LR_b_norho (mk_tycontext temp var ret gt gs) e1 lr = true ->
  (@eq (option mpred)) (nth_error R n) (Some (data_at sh t_root v' p')) ->
  (forall rho,
      !!(tc_environ (mk_tycontext temp var ret gt gs) rho) && (assertD P (localD T1 T2) R rho) |-- !! (p = p')) ->
  proj_val t_root gfs v' = v ->
  assertD P (localD (PTree.set id v T1) T2) R = Post ->
  nested_efield e1 efs tts = e0 ->

  (forall rho,
      !! (tc_environ (mk_tycontext temp var ret gt gs) rho) && (assertD P (localD T1 T2) R rho) |--
        !! (tc_val (typeof e0) v) &&
        !! (legal_nested_field t_root gfs)) ->
 semax (mk_tycontext temp var ret gt gs) (|> assertD P (localD T1 T2) R)
        (Sset id e0)
          (normal_ret_assert Post).
Proof.
  intros.
  subst Post e0.
  eapply semax_extract_later_prop'.
  Focus 1. {
    rewrite <- insert_local.
    exact H7.
  } Unfocus.
  intro; subst; clear H7.
  eapply semax_PTree_load with (gfs2 := gfs) (gfs0 := nil) (gfs1 := gfs) (t_root0 := t_root) (sh0 := sh);  eauto.
  + rewrite app_nil_r; reflexivity.
  + unfold assertD, localD, LocalD; simpl; intros. entailer!.
  + reflexivity.
  + repeat apply andp_right.
    - apply andp_left2. eapply tc_LR_b_sound; [eauto | | eauto].
      eapply nth_error_prop with (n := n); eauto.
      rewrite data_at_isptr.
      unfold assertD; entailer!.
    - intros rho.
      apply (derives_trans _ _ _ (H11 rho)).
      normalize.
    - intro rho.
      unfold local, lift1; simpl; apply prop_right.
      apply tc_efield_b_sound; auto.
  + intros rho.
    apply (derives_trans _ _ _ (H11 rho)).
    normalize.
Qed.

Definition load_lemma (temp : PTree.t (type * bool)) (var : PTree.t type)
     (ret : type) (gt : PTree.t type) (id : ident) (t t_root : type) (e0 e1 : Clight.expr)
    (efs: list efield) (tts : list type) (e : type_id_env) (lr : LLRR)
    (n: nat): my_lemma.
reify_lemma reify_vst (semax_load_localD temp var ret gt id t t_root e0 e1 efs tts e lr n).
Defined.

Lemma semax_store_localD:
    forall (temp : PTree.t (type * bool)) (var : PTree.t type)
     (ret : type) (gt : PTree.t type) (t t_root : type) (e0 e1 e2: Clight.expr)
     (efs : list efield) (tts : list type)
     (e : type_id_env) (lr : LLRR) (n: nat)
     sh P T1 T2 R gs Post
      (gfs: list gfield)
      (p p': val) (v0: val) (v': reptype t_root),
  forall {Espec: OracleKind},
      typeof (nested_efield e1 efs tts) = t ->
      type_is_by_value t = true ->
      tc_LR_b_norho (mk_tycontext temp var ret gt gs) e1 lr = true ->
      tc_LR_b_norho (mk_tycontext temp var ret gt gs) (Ecast e2 (typeof (nested_efield e1 efs tts))) RRRR = true ->
      tc_efield_b_norho (mk_tycontext temp var ret gt gs) efs = true ->
      msubst_efield_denote T1 T2 efs = Some gfs ->
      msubst_eval_LR T1 T2 e1 lr = Some p ->
      msubst_eval_LR T1 T2 (Ecast e2 t) RRRR = Some v0 ->
      legal_nested_efield e t_root e1 gfs tts lr = true ->

      (@eq (option mpred)) (nth_error R n) (Some (data_at sh t_root v' p')) ->
  (forall rho,
      !!(tc_environ (mk_tycontext temp var ret gt gs) rho) && (assertD P (localD T1 T2) R rho) |-- !! (p = p')) ->
  (forall rho,
      !! (tc_environ (mk_tycontext temp var ret gt gs) rho) && (assertD P (localD T1 T2) R rho) |--
        !! (legal_nested_field t_root gfs)) ->
  (assertD P (localD T1 T2)
                  (replace_nth n R
                    (data_at sh t_root
                      (upd_val t_root gfs v' v0) p))) = Post -> (* need to add replace_nth *)
      writable_share sh ->
  nested_efield e1 efs tts = e0 ->

      semax (mk_tycontext temp var ret gt gs) (|>assertD P (localD T1 T2) R)
        (Sassign e0 e2)
          (normal_ret_assert Post).
Proof.
  intros.
  assert (Post = assertD P (localD T1 T2)
          (replace_nth n R
             (field_at sh t_root []
                (upd_reptype (nested_field_type2 t_root nil) gfs v'
                   (valinject _ v0)) p))); [| clear H11].
  Focus 1. {
    unfold upd_val in H11.
    rewrite <- data_at_field_at.
    subst Post.
    f_equal.
  } Unfocus.
  subst Post e0.
  eapply semax_extract_later_prop'.
  Focus 1. {
    rewrite <- insert_local.
    exact H9.
  } Unfocus.
  intro; subst; clear H9.
  unfold upd_val.
  eapply semax_PTree_store with (gfs2 := gfs) (gfs0 := nil) (gfs1 := gfs) (t_root0 := t_root) (sh0 := sh);  eauto.
  + rewrite app_nil_r; reflexivity.
  + unfold assertD, localD, LocalD; simpl; intros. entailer!.
  + repeat apply andp_right.
    - apply andp_left2. eapply tc_LR_b_sound; [eauto | | eauto].
      eapply nth_error_prop with (n := n); eauto.
      rewrite data_at_isptr.
      unfold assertD; entailer!.
    - intro rho.
      apply prop_right.
      eapply tc_expr_b_sound; auto.
    - intro rho.
      unfold local, lift1; simpl; apply prop_right.
      apply tc_efield_b_sound; auto.
Qed.

Definition store_lemma (temp : PTree.t (type * bool)) (var : PTree.t type)
     (ret : type) (gt : PTree.t type) (t t_root : type) (e0 e1 e2: Clight.expr)
     (efs : list efield) (tts : list type)
     (e : type_id_env) (lr : LLRR) (n: nat): my_lemma.
reify_lemma reify_vst (semax_store_localD temp var ret gt t t_root e0 e1 e2 efs tts e lr n).
Defined.

(* Print store_lemma. *)

Section tbled.
Variable n : nat.
Variable tbl : SymEnv.functions RType_typ.

Let RSym_sym := RSym_sym tbl.
Existing Instance RSym_sym.

Let Expr_expr_fs := Expr_expr_fs tbl.
Existing Instance Expr_expr_fs.

Let Expr_ok_fs := Expr_ok_fs tbl.
Existing Instance Expr_ok_fs.

Let ExprVar_expr := @ExprVariables.ExprVar_expr typ func.
Existing Instance ExprVar_expr.

Existing Instance MA.

Existing Instance rtac_base.MentionsAnyOk.

Lemma load_store_sound_aux:
  forall t_root, (@funcAs typ func RType_typ
              (func_defs.RSym_sym tbl)
              (@inr
                 (sum
                    (sum SymEnv.func
                       (ModularFunc.ILogicFunc.ilfunc
                       typ))
                    (BILogicFunc.bilfunc typ))
                 func' (Sep (fdata_at t_root)))
              (tyArr tyshare
                 (tyArr
                    (reptyp t_root)
                    (tyArr tyval tympred))) =
            Some
              (fun (sh : share) (rt : typD (reptyp t_root)) (v : val) =>
               data_at sh t_root (reptyp_reptype t_root rt) v)).
Proof.
  intros.
  unfold funcAs; simpl.
  assert (forall pl: (fun t0 : typ =>
    {tyArr t0 (tyArr (reptyp t_root) (tyArr tyval tympred)) =
     tyArr tyshare (tyArr (reptyp t_root) (tyArr tyval tympred))} +
    {tyArr t0 (tyArr (reptyp t_root) (tyArr tyval tympred)) <>
     tyArr tyshare (tyArr (reptyp t_root) (tyArr tyval tympred))})
     tyshare, pl = left eq_refl).
  Focus 1. {
    intros.
    destruct pl; [f_equal; apply proof_irr | congruence].
  } Unfocus.
  match goal with
  | [ |- context [match (match ?e with _ => _ end) with _ => _ end] ] => rewrite (H e)
  end.
  unfold Rcast; simpl.
  reflexivity.
Qed.

Lemma APPLY_sound_store_lemma: forall (temp : PTree.t (type * bool)) (var : PTree.t type)
  (ret : type) (gt : PTree.t type) (t t_root : type)
  (e0 e1 e2 : Clight.expr) (efs : list efield) (tts : list type)
  (e : type_id_env) (lr : LLRR) (n : nat),
  rtac_sound (EAPPLY typ func (store_lemma temp var ret gt t t_root e0 e1 e2 efs tts e lr n)).
Proof.
  intros.
  apply EAPPLY_sound; auto with typeclass_instances.
  + apply APPLY_condition1.
  + apply APPLY_condition2.
  + unfold Lemma.lemmaD, split_env, Lemma.lemmaD'. simpl.
    unfold exprD'_typ0. simpl.
    unfold exprD'. simpl.

    rewrite (load_store_sound_aux t_root); simpl.
    assert (@funcAs typ func RType_typ
                (func_defs.RSym_sym tbl)
                (@inr
                (sum
                (sum SymEnv.func
                (ILogicFunc.ilfunc typ))
                (BILogicFunc.bilfunc typ))
                func'
                (Sep (fupd_val t_root)))
                (tyArr
                (tylist tygfield)
                (tyArr
                (reptyp t_root)
                (tyArr tyval
                (reptyp t_root))))
      = Some
         (fun (gfs : list gfield) (v : typD (reptyp t_root)) (v0 : val) =>
          reptype_reptyp t_root (upd_val t_root gfs (reptyp_reptype t_root v) v0))).
    Focus 1. {
      intros.
      unfold funcAs.
      simpl.
      assert (forall pl: (fun t0 : typ =>
        {tyArr t0 (tyArr (reptyp t_root) (tyArr tyval (reptyp t_root))) =
         tyArr (tylist tygfield)
           (tyArr (reptyp t_root) (tyArr tyval (reptyp t_root)))} +
        {tyArr t0 (tyArr (reptyp t_root) (tyArr tyval (reptyp t_root))) <>
         tyArr (tylist tygfield)
           (tyArr (reptyp t_root) (tyArr tyval (reptyp t_root)))})
         (tylist tygfield), pl = left eq_refl).
      Focus 1. {
        intros.
        destruct pl; [f_equal; apply proof_irr | congruence].
      } Unfocus.
      match goal with
      | [ |- context [match (match ?e with _ => _ end) with _ => _ end] ] => rewrite (H e)
      end.
      unfold Rcast; simpl.
      reflexivity.
    } Unfocus.
    rewrite H. simpl. clear H.
    intros.
    unfold exprT_App, exprT_Inj, Rcast_val, Rcast in *. simpl in *.
    unfold ModularFunc.ILogicFunc.typ2_cast_quant, ModularFunc.ILogicFunc.typ2_cast_bin in *; simpl in *.
    eapply semax_store_localD; eauto.
    rewrite reptyp_reptype_reptype_reptyp in H11.
    exact H11.
Qed.

Lemma APPLY_sound_load_lemma: forall (temp : PTree.t (type * bool)) (var : PTree.t type)
  (ret : type) (gt : PTree.t type) (id : ident) (t t_root : type)
  (e0 e1 : Clight.expr) (efs : list efield) (tts : list type)
  (e : type_id_env) (lr : LLRR) (n : nat),
  rtac_sound (EAPPLY typ func (load_lemma temp var ret gt id t t_root e0 e1 efs tts e lr n)).
Proof.
  intros.
  apply EAPPLY_sound; auto with typeclass_instances.
  + apply APPLY_condition1.
  + apply APPLY_condition2.
  + unfold Lemma.lemmaD, split_env, Lemma.lemmaD'. simpl.
(* Set Printing Depth 200. *)
    unfold exprD'_typ0. simpl.
    unfold exprD'. simpl.
    rewrite (load_store_sound_aux t_root); simpl.
    assert (exprT_GetVAs []
                  [tyOracleKind;
                reptyp t_root; tyval; tyval; tyval;
                tylist tygfield;
                tyArr tyenviron tympred;
                tylist tympred;
                typtree (typrod tyc_type tyval);
                typtree tyval;
                tylist typrop; tyshare;
                typtree tyfunspec] 1
                (reptyp t_root) = Some
      (fun (_ : HList.hlist typD [])
         (vs : HList.hlist typD
                [tyOracleKind; reptyp t_root; tyval; tyval; tyval;
                tylist tygfield; tyArr tyenviron tympred;
                tylist tympred; typtree (typrod tyc_type tyval);
                typtree tyval; tylist typrop; tyshare;
                typtree tyfunspec]) => HList.hlist_hd (HList.hlist_tl vs))).
    Focus 1. {
      intros.
      unfold exprT_GetVAs. simpl.
      destruct (typ_eq_dec (reptyp t_root) (reptyp t_root)); [ |congruence].
      assert (e2 = eq_refl) by apply proof_irr.
      subst.
      unfold Rcast_val, Rcast; simpl.
    reflexivity.
    } Unfocus.
    rewrite H. simpl; clear H.
    intros.
    unfold exprT_App, exprT_Inj, Rcast_val, Rcast in *. simpl in *.
    unfold ModularFunc.ILogicFunc.typ2_cast_quant, ModularFunc.ILogicFunc.typ2_cast_bin in *; simpl in *.
    eapply semax_load_localD; eauto.
Qed.

End tbled.

author: PrincetonUniversity

repo: VST


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

(* TODO : change this to field once field isomorphism happens *)
Definition carry :
  { carry : feBW_loose -> feBW_tight
  | forall a, phiBW_tight (carry a) = (phiBW_loose a) }.
Proof.
  Set Ltac Profiling.
  Time synthesize_carry ().
  Show Ltac Profile.
Time Defined.

Print Assumptions carry.


text:
Set Implicit Arguments.

Require Import Platform.Cito.NoUninitDec.

Require Platform.Cito.Wf.
Require Import Coq.Bool.Bool.

Require Import Platform.Cito.GeneralTactics2.

Require Import Coq.Lists.List.
Import ListNotations.
Local Open Scope list_scope.

Require Import Bedrock.StringSet.
Import StringSet.
Require Import Platform.Cito.StringSetFacts.
Import FSetNotations.
Import FSetNotationsTrial.
Local Open Scope fset_scope.

Lemma inits_elim stmt : forall x, In x (inits stmt) -> Wf.writes stmt x.
Proof.
  induction stmt; simpl; intros x Hin.
  - eapply empty_iff in Hin; eauto.
  - eapply union_iff in Hin.
    destruct Hin as [Hin | Hin].
    + left; eauto.
    + right; eauto.
  - eapply inter_iff in Hin.
    destruct Hin as [Hin1 Hin2].
    eauto.
  - eapply empty_iff in Hin; eauto.
  - destruct o as [lhs|]; simpl in *.
    + eapply singleton_iff in Hin.
      eauto.
    + eapply empty_iff in Hin; eauto.
  - eapply singleton_iff in Hin.
    eauto.
  - eapply singleton_iff in Hin.
    eauto.
Qed.

Require Import Platform.Cito.GeneralTactics Platform.Cito.GeneralTactics4.

Require Import Platform.Cito.FreeVarsExpr.

Lemma expReads_free_vars e : forall uninited x, Wf.expReads uninited e x -> In x (free_vars e) /\ uninited x.
Proof.
  induction e; simpl; intros uninited x Hr.
  - openhyp.
    split; eauto.
    eapply singleton_iff; eauto.
  - intuition.
  - destruct Hr as [Hr | Hr].
    + eapply IHe1 in Hr.
      openhyp.
      split; eauto.
      eapply union_iff; eauto.
    + eapply IHe2 in Hr.
      openhyp.
      split; eauto.
      eapply union_iff; eauto.
  - destruct Hr as [Hr | Hr].
    + eapply IHe1 in Hr.
      openhyp.
      split; eauto.
      eapply union_iff; eauto.
    + eapply IHe2 in Hr.
      openhyp.
      split; eauto.
      eapply union_iff; eauto.
Qed.

Definition disj uninited inited := forall x, uninited x -> In x inited -> False.

Lemma expReads_free_vars_diff e x uninited inited : Wf.expReads uninited e x -> disj uninited inited -> In x (free_vars e - inited).
Proof.
  intros Hr Hdisj.
  eapply diff_iff.
  eapply expReads_free_vars in Hr.
  openhyp; split; eauto.
Qed.

Require Import Coq.Strings.String.

Definition sub_set (a : string -> Prop) b := forall x, a x -> In x b.

Lemma ExistsR_fold_left' elt (ls : list elt) : forall a0 b0 a b all, sub_set a0 b0 -> (forall e, sub_set (a e) (b e)) -> (forall x, all x <-> (a0 x \/ Wf.ExistsR (fun e => a e x) ls)) -> sub_set all (fold_left (fun acc e => b e + acc) ls b0).
Proof.
  induction ls; simpl; intros a0 b0 af bf all Hss0 Hss Heq.
  - unfold sub_set in *.
    intros x Hin.
    eapply Heq in Hin.
    openhyp; intuition.
  - eapply IHls; eauto.
    + instantiate (1 := fun x => a0 x \/ af a x).
      unfold sub_set in *.
      intros x Ha.
      eapply union_iff.
      intuition.
    + intros x.
      etransitivity.
      eauto.
      intuition.
Qed.

Lemma ExistsR_fold_left elt (ls : list elt) : forall a0 b0 a b, sub_set a0 b0 -> (forall e, sub_set (a e) (b e)) -> sub_set (fun x => a0 x \/ Wf.ExistsR (fun e => a e x) ls) (fold_left (fun acc e => b e + acc) ls b0).
Proof.
  intros.
  eapply ExistsR_fold_left'; eauto.
  intuition.
Qed.

Lemma uninited_reads_intro' stmt : forall x uninited inited, Wf.reads uninited stmt x -> disj uninited inited -> In x (uninited_reads inited stmt).
Proof.
  induction stmt; simpl; intros x uninited inited Hr Hdisj.
  - eapply empty_iff; eauto.
  - eapply union_iff.
    destruct Hr as [Hr1 | Hr2].
    + left.
      eauto.
    + right.
      eapply IHstmt2; eauto.
      intros x' Hu Hi.
      simpl in *.
      eapply union_iff in Hi.
      destruct Hu as [Hu Hnw].
      destruct Hi as [Hi | Hi].
      * eauto.
      * contradict Hnw.
        eapply inits_elim; eauto.
  - eapply union_iff.
    destruct Hr as [Hr | [Hr | Hr]].
    + left.
      eapply union_iff.
      left.
      eapply expReads_free_vars_diff; eauto.
    + left.
      eapply union_iff.
      right.
      eauto.
    + right.
      eauto.
  - eapply union_iff.
    destruct Hr as [Hr | Hr].
    + left.
      eapply expReads_free_vars_diff; eauto.
    + right.
      eauto.
  - eapply ExistsR_fold_left; eauto; unfold sub_set in *.
    intros; eapply expReads_free_vars_diff; eauto.
    intros; eapply expReads_free_vars_diff; eauto.
  - eapply empty_iff; eauto.
  - eapply expReads_free_vars_diff; eauto.
Qed.

Lemma uninited_reads_intro stmt : forall x inited, Wf.reads (fun x => ~ List.In x inited) stmt x -> In x (uninited_reads (of_list inited) stmt).
Proof.
  intros.
  eapply uninited_reads_intro'; eauto.
  unfold disj.
  intros x' Hni Hi.
  eapply of_list_fwd in Hi.
  intuition.
Qed.

Require Import Platform.Cito.FuncCore.

Lemma is_no_uninited_reads_sound f : is_no_uninited_reads f = true -> forall x, ~ Wf.reads (fun x => ~ List.In x (ArgVars f)) (Body f) x.
Proof.
  intros Hb x.
  unfold is_no_uninited_reads in *.
  nintro.
  eapply uninited_reads_intro in H.
  eapply is_empty_iff in Hb.
  contradict H.
  eauto.
Qed.

Lemma is_no_uninited_sound f : is_no_uninited f = true -> Wf.NoUninitialized (ArgVars f) (RetVar f) (Body f).
Proof.
  intros Hb.
  unfold is_no_uninited, Wf.NoUninitialized in *.
  eapply andb_true_iff in Hb.
  destruct Hb as [Hnur Hr].
  split.
  eapply is_no_uninited_reads_sound; eauto.
  eapply mem_iff in Hr.
  eapply inits_elim; eauto.
Qed.

author: JasonGross


text:
(**************************************************************)
(*   Copyright                                                *)
(*             Jean-François Monin           [+]              *)
(*                                                            *)
(*            [+] Affiliation VERIMAG - Univ. Grenoble-Alpes  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

(* A lightweight tactic for marking terms at given places *)

Definition MARQ {A: Type} (x:A) := x.

Tactic Notation "mark" constr(i) "at" integer_list(l) :=
  pattern i at l;
  match goal with |- ?f ?x => change (f (MARQ x)) end;
  cbv beta.

Tactic Notation "mark" constr(i) "at" ne_integer_list(l) "in" hyp(H) :=
  pattern i at l in H;
  match type of H with ?f ?x => change (f (MARQ x)) in H end;
  cbv beta in H.

author: DmxLarchey

repo: The-Braga-Method


text:
From Undecidability.L.Tactics Require Import LTactics.
From Undecidability.L Require Import UpToC.
From Undecidability.L Require Import Functions.EqBool.

From Undecidability.L.Datatypes Require Export List.List_enc LBool LOptions LNat.

Set Default Proof Using "Type".

Section Fix_X.
  Variable (X:Type).
  Context {intX : registered X}.

  Fixpoint inb eqb (x:X) (A: list X) :=
    match A with
      nil => false
    | a::A' => orb (eqb a x) (inb eqb x A')
    end.

  Variable X_eqb : X -> X -> bool.
  Hypothesis X_eqb_spec : (forall (x y:X), Bool.reflect (x=y) (X_eqb x y)).

  Lemma inb_spec: forall x A, Bool.reflect (In x A) (inb X_eqb x A).
  Proof using X_eqb_spec.
    intros x A. induction A.
    -constructor. tauto.
    -simpl. destruct (X_eqb_spec a x).
    +constructor. tauto.
    +inv IHA. destruct (X_eqb_spec a x).
      *constructor. tauto.
      *constructor. tauto.
      *constructor. tauto.
  Qed.

  Global Instance term_inb: computableTime' inb (fun eq eqT => (5,fun x _ => (1,fun l _ =>
                                        (fold_right (fun x' res => callTime2 eqT x' x
                                                                + res + 17) 4 l ,tt)))).
  Proof.
    extract.
    solverec.
  Defined.

  Global Instance term_inb_notime: computable inb.
  Proof.
    extract.
  Defined.

End Fix_X.

Section list_eqb.

  Variable X : Type.
  Variable eqb : X -> X -> bool.
  Variable spec : forall x y, reflect (x = y) (eqb x y).

  Fixpoint list_eqb A B :=
    match A,B with
    | nil,nil => true
    | a::A',b::B' => eqb a b && list_eqb A' B'
    | _,_ => false
    end.

  Lemma list_eqb_spec A B : reflect (A = B) (list_eqb A B).
  Proof using spec.
    revert B; induction A; intros; destruct B; cbn in *; try now econstructor.
    destruct (spec a x), (IHA B); cbn; econstructor; congruence.
  Qed.

End list_eqb.

Section int.

  Context {X : Type}.
  Context {HX : registered X}.

  Fixpoint list_eqbTime (eqbT: timeComplexity (X -> X -> bool)) (A B:list X) :=
    match A,B with
      a::A,b::B => callTime2 eqbT a b + 22 + list_eqbTime eqbT A B
    | _,_ => 9
    end.

  Global Instance term_list_eqb : computableTime' (list_eqb (X:=X))
                                                  (fun _ eqbT => (1,(fun A _ => (5,fun B _ => (list_eqbTime eqbT A B,tt))))).
  Proof.
    extract.
    solverec.
  Defined.

  Definition list_eqbTime_leq (eqbT: timeComplexity (X -> X -> bool)) (A B:list X) k:
    (forall a b, callTime2 eqbT a b <= k)
    -> list_eqbTime eqbT A B <= length A * (k+22) + 9.
  Proof.
    intros H'. induction A in B|-*.
    -cbn. lia.
    -destruct B.
    {cbn. intuition. }
    cbn - [callTime2]. setoid_rewrite IHA.
    rewrite H'. ring_simplify. intuition.
  Qed.

  Lemma list_eqbTime_bound_r (eqbT : timeComplexity (X -> X -> bool)) (A B : list X) f:
    (forall (x y:X), callTime2 eqbT x y <= f y) ->
    list_eqbTime eqbT A B <= sumn (map f B) + 9 + length B * 22.
  Proof.
    intros H.
    induction A in B|-*;unfold list_eqbTime;fold list_eqbTime. now Lia.lia.
    destruct B.
    -cbn. Lia.lia.
    -rewrite H,IHA. cbn [length map sumn]. Lia.lia.
  Qed.

  Global Instance eqbList f `{eqbClass (X:=X) f}:
    eqbClass (list_eqb f).
  Proof.
    intros ? ?. eapply list_eqb_spec. all:eauto using eqb_spec.
  Qed.
  Import EqBool.
  Global Instance eqbComp_List `{eqbCompT X (R:=HX)}:
    eqbCompT (list X).
  Proof.
    evar (c:nat). exists c. unfold list_eqb.
    unfold enc;cbn.
    change (eqb0) with (eqb (X:=X)).
    extract. unfold eqb,eqbTime. fold @enc.
    recRel_prettify2. easy.
    [c]:exact (c__eqbComp X + 6).
    all:unfold c. all:cbn iota beta delta [list_enc].
    all:  change ((match HX with
                  | @mk_registered _ enc _ _ => enc
                  end)) with (enc (X:=X)).
    all:cbn [size]. all: nia.
  Qed.

End int.

author: uds-psl