text:
(* Ps_mul.v *)

Require Import Utf8.
Require Import QArith.
Require Import NPeano.

Require Import Misc.
Require Import NbarM.
Require Import Field2.
Require Import Fsummation.
Require Import Power_series.
Require Import Puiseux_series.
Require Import Ps_add.
Require Import Ps_add_compat.

Set Implicit Arguments.

(* ps_mul *)

Definition ps_mul {α} {r : ring α} ps₁ ps₂ :=
  {| ps_terms :=
       series_mul
         (series_stretch (cm_factor ps₁ ps₂) (ps_terms ps₁))
         (series_stretch (cm_factor ps₂ ps₁) (ps_terms ps₂));
     ps_ordnum :=
       (ps_ordnum ps₁ * Zpos (ps_polydo ps₂) + ps_ordnum ps₂ * Zpos (ps_polydo ps₁))%Z;
     ps_polydo :=
       cm ps₁ ps₂ |}.

Notation "a * b" := (ps_mul a b) : ps_scope.

Section theorems_for_mul.

Variable α : Type.
Variable r : ring α.
Variable K : field r.

Theorem ps_normal_mul_comm : ∀ ps₁ ps₂,
  normalise_ps (ps₁ * ps₂)%ps ≐ normalise_ps (ps₂ * ps₁)%ps.
Proof.
intros ps₁ ps₂.
unfold normalise_ps; simpl.
remember (series_stretch (cm_factor ps₁ ps₂) (ps_terms ps₁)) as s₁ eqn:Hs₁ .
remember (series_stretch (cm_factor ps₂ ps₁) (ps_terms ps₂)) as s₂ eqn:Hs₂ .
rewrite series_mul_comm.
remember (series_order (s₂ * s₁)%ser 0) as n eqn:Hn .
destruct n as [n| ]; [ idtac | reflexivity ].
constructor; simpl.
 unfold gcd_ps; simpl.
 rewrite series_mul_comm.
 f_equal; [ f_equal; apply Z.add_comm | f_equal ].
 f_equal; [ f_equal; apply Z.add_comm | idtac ].
 unfold cm; rewrite Pos.mul_comm; reflexivity.

 unfold cm; rewrite Pos.mul_comm, series_mul_comm.
 unfold gcd_ps; simpl.
 do 3 f_equal.
 f_equal; [ f_equal; apply Z.add_comm | idtac ].
 unfold cm; rewrite Pos.mul_comm; reflexivity.

 unfold gcd_ps; simpl.
 unfold cm; rewrite Pos.mul_comm, series_mul_comm.
 remember (ps_ordnum ps₁ * Zpos (ps_polydo ps₂))%Z as x eqn:Hx .
 remember (ps_ordnum ps₂ * Zpos (ps_polydo ps₁))%Z as y eqn:Hy .
 replace (x + y)%Z with (y + x)%Z by apply Z.add_comm.
 reflexivity.
Qed.

Theorem ps_mul_comm : ∀ ps₁ ps₂, (ps₁ * ps₂ = ps₂ * ps₁)%ps.
Proof.
intros ps₁ ps₂.
constructor.
apply ps_normal_mul_comm.
Qed.

Theorem ps_mul_1_l : ∀ ps, (1 * ps = ps)%ps.
Proof.
intros ps.
constructor.
unfold normalise_ps; simpl.
unfold cm, cm_factor; simpl.
rewrite stretch_series_1, series_mul_1_l.
rewrite series_stretch_1.
remember (series_order (ps_terms ps) 0) as n eqn:Hn .
symmetry in Hn.
destruct n as [n| ]; [ idtac | reflexivity ].
constructor; simpl.
 rewrite Z.mul_1_r; f_equal.
 rewrite stretch_series_1, series_stretch_1, series_mul_1_l.
 unfold gcd_ps; simpl.
 rewrite Z.mul_1_r; reflexivity.

 do 2 f_equal.
 rewrite stretch_series_1, series_stretch_1, series_mul_1_l.
 unfold gcd_ps; simpl.
 rewrite Z.mul_1_r; reflexivity.

 do 2 rewrite stretch_series_1 in |- * at 1.
 do 2 rewrite series_stretch_1 in |- * at 1.
 rewrite series_mul_1_l.
 unfold gcd_ps; simpl.
 rewrite Z.mul_1_r; reflexivity.
Qed.

Theorem ps_mul_1_r : ∀ ps, (ps * 1 = ps)%ps.
Proof. intros ps. rewrite ps_mul_comm. apply ps_mul_1_l. Qed.

Theorem series_order_series_0 :
  series_order 0%ser 0 = ∞.
Proof.
apply series_order_iff; intros i.
rewrite series_nth_series_0; reflexivity.
Qed.

Theorem ps_mul_0_l : ∀ ps, (0 * ps = 0)%ps.
Proof.
intros ps.
constructor.
unfold normalise_ps; simpl.
unfold cm_factor; simpl.
rewrite series_stretch_series_0.
rewrite series_mul_0_l.
rewrite series_order_series_0.
reflexivity.
Qed.

Theorem ps_mul_0_r : ∀ ps, (ps * 0 = 0)%ps.
Proof. intros ps. rewrite ps_mul_comm. apply ps_mul_0_l. Qed.

Theorem series_stretch_mul : ∀ a b k,
  (series_stretch k (a * b) =
   series_stretch k a * series_stretch k b)%ser.
Proof.
intros a b k.
constructor; intros i; simpl.
destruct (zerop (i mod Pos.to_nat k)) as [H₂| H₂].
 apply Nat.mod_divides in H₂; auto with Arith.
 destruct H₂ as (c, Hc).
 rewrite Hc.
 rewrite Nat.mul_comm.
 rewrite Nat.div_mul; auto with Arith.
 unfold convol_mul; simpl.
 rename k into n, i into k.
 symmetry.
 apply inserted_0_summation; auto with Arith.
  intros i Hi.
  destruct (zerop (i mod Pos.to_nat n)) as [| H₂]; [ contradiction | idtac ].
  rewrite rng_mul_0_l; reflexivity.

  intros i.
  rewrite Nat.mul_comm.
  rewrite <- Nat.mul_sub_distr_r.
  rewrite Nat.mod_mul; auto with Arith; simpl.
  rewrite Nat.mod_mul; auto with Arith; simpl.
  rewrite Nat.div_mul; auto with Arith; simpl.
  rewrite Nat.div_mul; auto with Arith; simpl.

 unfold convol_mul.
 symmetry.
 apply all_0_summation_0; intros j Hj.
 destruct (zerop (j mod Pos.to_nat k)) as [H₄| H₄].
  destruct (zerop ((i - j) mod Pos.to_nat k)) as [H₅| H₅].
   apply Nat.mod_divides in H₄; auto with Arith.
   apply Nat.mod_divides in H₅; auto with Arith.
   destruct H₄ as (c, Hc).
   destruct H₅ as (d, Hd).
   subst j.
   apply Nat.add_sub_eq_nz in Hd.
    subst i.
    rewrite <- Nat.mul_add_distr_l in H₂; auto with Arith.
    rewrite Nat.mul_comm in H₂.
    rewrite Nat.mod_mul in H₂; auto with Arith.
    exfalso; revert H₂; apply Nat.lt_irrefl.

    intros H.
    rewrite H in Hd.
    apply Nat.sub_0_le in Hd.
    destruct Hj as (_, Hj).
    apply Nat.le_antisymm in Hd; auto with Arith.
    rewrite <- Hd in H₂.
    rewrite Nat.mul_comm in H₂.
    rewrite Nat.mod_mul in H₂; auto with Arith.
    exfalso; revert H₂; apply Nat.lt_irrefl.

   rewrite rng_mul_comm.
   rewrite shifted_in_stretched; [ idtac | assumption ].
   rewrite rng_mul_0_l; reflexivity.

  rewrite shifted_in_stretched; [ idtac | assumption ].
  rewrite rng_mul_0_l; reflexivity.
Qed.

Theorem ps_mul_assoc : ∀ ps₁ ps₂ ps₃,
  (ps₁ * (ps₂ * ps₃) = (ps₁ * ps₂) * ps₃)%ps.
Proof.
intros ps₁ ps₂ ps₃.
constructor.
unfold normalise_ps; simpl.
rewrite series_stretch_mul; symmetry.
rewrite series_stretch_mul; symmetry.
do 4 rewrite <- series_stretch_stretch.
unfold cm, cm_factor; simpl.
rewrite series_mul_assoc.
remember (ps_polydo ps₂ * ps_polydo ps₃)%positive as c₂₃ eqn:Hc₂₃ .
remember (ps_polydo ps₃ * ps_polydo ps₁)%positive as c₃₁ eqn:Hc₃₁ .
remember (ps_polydo ps₁ * ps_polydo ps₂)%positive as c₁₂ eqn:Hc₁₂ .
rewrite Pos.mul_comm in Hc₂₃; rewrite <- Hc₂₃.
rewrite Pos.mul_comm in Hc₃₁; rewrite <- Hc₃₁.
remember (series_stretch c₂₃ (ps_terms ps₁)) as s₁ eqn:Hs₁ .
remember (series_stretch c₃₁ (ps_terms ps₂)) as s₂ eqn:Hs₂ .
remember (series_stretch c₁₂ (ps_terms ps₃)) as s₃ eqn:Hs₃ .
remember (series_mul (series_mul s₁ s₂) s₃) as s₁₂₃ eqn:Hs₁₂₃ .
remember (series_order s₁₂₃ 0) as n eqn:Hn .
symmetry in Hn.
destruct n as [n| ]; [ idtac | reflexivity ].
unfold gcd_ps; simpl.
progress unfold cm; simpl.
progress unfold cm; simpl.
do 2 rewrite Z.mul_add_distr_r.
do 6 rewrite Pos2Z.inj_mul.
do 3 rewrite Z.mul_assoc.
do 2 rewrite Z.add_assoc.
constructor; simpl.
 f_equal.
  f_equal.
  f_equal.
   f_equal.
    rewrite Hc₂₃, Pos2Z.inj_mul, Z.mul_assoc, Z.mul_shuffle0.
    reflexivity.

    rewrite Z.mul_shuffle0; reflexivity.

   rewrite Hc₁₂, Pos2Z.inj_mul, Z.mul_assoc, Z.mul_shuffle0.
   reflexivity.

  f_equal.
   do 2 f_equal.
   f_equal; [ f_equal | idtac ]; apply Z.mul_shuffle0.

   do 2 rewrite series_stretch_mul.
   do 4 rewrite <- series_stretch_stretch.
   rewrite <- Hc₁₂, <- Hc₂₃, <- Hc₃₁.
   rewrite Pos.mul_comm, <- Hc₃₁.
   rewrite <- Hs₁, <- Hs₂, <- Hs₃.
   rewrite series_mul_assoc; reflexivity.

 do 2 f_equal.
 f_equal.
  do 2 f_equal.
  f_equal; [ f_equal | idtac ]; apply Z.mul_shuffle0.

  do 2 rewrite series_stretch_mul.
  do 4 rewrite <- series_stretch_stretch.
  rewrite <- Hc₁₂, <- Hc₂₃, <- Hc₃₁.
  rewrite Pos.mul_comm, <- Hc₃₁.
  rewrite <- Hs₁, <- Hs₂, <- Hs₃.
  rewrite series_mul_assoc; reflexivity.

 constructor; intros i.
 do 4 rewrite series_stretch_mul at 1.
 do 8 rewrite <- series_stretch_stretch at 1.
 rewrite <- Hc₁₂, <- Hc₂₃, <- Hc₃₁.
 rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul, Pos.mul_comm, <- Hc₂₃.
 rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul, Pos.mul_comm, <- Hc₃₁.
 rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul, Pos.mul_comm, <- Hc₁₂.
 symmetry.
 rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul, <- Hc₃₁.
 rewrite <- Z.mul_assoc, <- Pos2Z.inj_mul, <- Hc₁₂.
 rewrite series_mul_assoc.
 rewrite <- Hs₁, <- Hs₂, <- Hs₃.
 reflexivity.
Qed.

Theorem eq_strong_ps_mul_compat_r : ∀ ps₁ ps₂ ps₃,
  eq_ps_strong ps₁ ps₂
  → eq_ps_strong (ps_mul ps₁ ps₃) (ps_mul ps₂ ps₃).
Proof.
intros ps₁ ps₂ ps₃ Heq.
induction Heq.
constructor; simpl.
 rewrite H, H0; reflexivity.

 unfold cm; simpl.
 rewrite H0; reflexivity.

 unfold cm_factor.
 rewrite H0, H1.
 reflexivity.
Qed.

Theorem series_shift_mul : ∀ a b n,
  (series_shift n (a * b)%ser = series_shift n a * b)%ser.
Proof.
intros a b n.
constructor; intros k; simpl.
destruct (lt_dec k n) as [H₂| H₂].
 symmetry; unfold convol_mul; simpl.
 apply all_0_summation_0; intros i Hi.
 destruct (lt_dec i n) as [H₁| H₁].
  rewrite rng_mul_0_l; reflexivity.

  exfalso; apply H₁.
  eapply le_lt_trans; [ idtac | eassumption ].
  destruct Hi; assumption.

 apply Nat.nlt_ge in H₂.
 unfold convol_mul.
 symmetry.
 destruct n.
  rewrite Nat.sub_0_r.
  apply summation_compat; intros i Hi.
  rewrite series_shift_0; reflexivity.

  assert (k = (n + (k - n))%nat) as H by fast_omega H₂.
  rewrite H in |- * at 1.
  rewrite summation_ub_add.
  rewrite rng_add_comm.
  rewrite <- H.
  rewrite rng_add_comm.
  rewrite all_0_summation_0.
   rewrite rng_add_0_l.
   symmetry.
   rewrite summation_add_add_sub with (n := S n).
   rewrite Nat.add_0_l, Nat.sub_add; [ idtac | assumption ].
   apply summation_compat; intros i Hi.
   assert (i = i - S n + S n)%nat as H₁ by fast_omega Hi.
   rewrite H₁ in |- * at 3.
   rewrite series_nth_add_shift.
   rewrite <- Nat.sub_add_distr.
   rewrite Nat.add_comm.
   rewrite <- H₁; reflexivity.

   intros i Hi; simpl.
   destruct (lt_dec i (S n)) as [H₁| H₁].
    rewrite rng_mul_0_l; reflexivity.

    exfalso; apply H₁.
    apply Nat.lt_succ_r.
    destruct Hi; assumption.
Qed.

Theorem normalise_ps_mul_adjust_l : ∀ ps₁ ps₂ n k,
  normalise_ps (ps_mul ps₁ ps₂) ≐
  normalise_ps (ps_mul (adjust_ps n k ps₁) ps₂).
Proof.
intros ps₁ ps₂ n k.
remember (Pos.to_nat (ps_polydo ps₂) * n)%nat as m eqn:Hm .
rewrite ps_normal_adjust_eq with (n := m) (k := k); subst m.
unfold ps_mul; simpl.
unfold adjust_ps; simpl.
unfold cm, cm_factor; simpl.
rewrite Pos2Z.inj_mul, Z.mul_assoc.
rewrite Z.mul_sub_distr_r.
rewrite Z.mul_shuffle0.
rewrite <- Z.add_sub_swap.
rewrite <- Z.mul_add_distr_r.
rewrite Nat.mul_comm.
rewrite Nat2Z.inj_mul.
rewrite positive_nat_Z.
rewrite Pos_mul_shuffle0.
rewrite series_stretch_mul.
rewrite stretch_shift_series_distr.
do 3 rewrite <- series_stretch_stretch.
rewrite series_shift_mul.
rewrite Pos.mul_comm.
rewrite series_mul_comm, Pos.mul_comm, series_mul_comm.
reflexivity.
Qed.

Theorem ps_normal_mul_compat_r : ∀ ps₁ ps₂ ps₃,
  normalise_ps ps₁ ≐ normalise_ps ps₂
  → normalise_ps (ps_mul ps₁ ps₃) ≐ normalise_ps (ps_mul ps₂ ps₃).
Proof.
intros ps₁ ps₂ ps₃ Heq.
remember Heq as Heqv; clear HeqHeqv.
remember (normalise_ps ps₁) as nps₁ eqn:Hps₁  in Heq.
remember (normalise_ps ps₂) as nps₂ eqn:Hps₂  in Heq.
symmetry in Hps₁, Hps₂.
remember (series_order (ps_terms ps₁) 0) as m₁ eqn:Hm₁ .
remember (series_order (ps_terms ps₂) 0) as m₂ eqn:Hm₂ .
symmetry in Hm₁, Hm₂.
destruct m₁ as [m₁| ].
 apply normalised_exists_adjust in Hps₁.
  destruct m₂ as [m₂| ].
   apply normalised_exists_adjust in Hps₂.
    destruct Hps₁ as (n₁, (k₁, Hps₁)).
    destruct Hps₂ as (n₂, (k₂, Hps₂)).
    apply eq_strong_ps_mul_compat_r with (ps₃ := ps₃) in Hps₁.
    apply eq_strong_ps_mul_compat_r with (ps₃ := ps₃) in Hps₂.
    rewrite Hps₁, Hps₂.
    rewrite <- normalise_ps_mul_adjust_l.
    rewrite <- normalise_ps_mul_adjust_l.
    apply eq_strong_ps_mul_compat_r with (ps₃ := ps₃) in Heq.
    rewrite Heq; reflexivity.

    intros H; rewrite Hm₂ in H; discriminate H.

   symmetry in Heqv.
   eapply series_order_inf_compat in Hm₂; [ idtac | eassumption ].
   rewrite Hm₁ in Hm₂; discriminate Hm₂.

  intros H; rewrite Hm₁ in H; discriminate H.

 clear Hm₂.
 remember Hm₁ as Hm₂; clear HeqHm₂.
 eapply series_order_inf_compat in Hm₂; [ idtac | eassumption ].
 apply eq_strong_ps_adjust_zero_neg_zero in Hm₁.
 apply eq_strong_ps_adjust_zero_neg_zero in Hm₂.
 destruct Hm₁ as (n₁, (n₂, (k₁, (k₂, Hm₁)))).
 destruct Hm₂ as (n₃, (n₄, (k₃, (k₄, Hm₂)))).
 apply eq_strong_ps_mul_compat_r with (ps₃ := ps₃) in Hm₁.
 apply eq_strong_ps_mul_compat_r with (ps₃ := ps₃) in Hm₂.
 rewrite normalise_ps_mul_adjust_l with (n := n₁) (k := k₁).
 rewrite Hm₁; symmetry.
 rewrite normalise_ps_mul_adjust_l with (n := n₃) (k := k₃).
 rewrite Hm₂; symmetry.
 rewrite <- normalise_ps_mul_adjust_l.
 rewrite <- normalise_ps_mul_adjust_l.
 reflexivity.
Qed.

Theorem ps_mul_compat_r : ∀ ps₁ ps₂ ps₃,
  (ps₁ = ps₂)%ps
  → (ps₁ * ps₃ = ps₂ * ps₃)%ps.
Proof.
intros ps₁ ps₂ ps₃ H₁₂.
constructor.
apply ps_normal_mul_compat_r.
inversion H₁₂; assumption.
Qed.

Theorem ps_mul_compat_l : ∀ ps₁ ps₂ ps₃,
  (ps₁ = ps₂)%ps
  → (ps₃ * ps₁ = ps₃ * ps₂)%ps.
Proof.
intros ps₁ ps₂ ps₃ Heq.
rewrite ps_mul_comm; symmetry.
rewrite ps_mul_comm; symmetry.
apply ps_mul_compat_r; assumption.
Qed.

End theorems_for_mul.

Add Parametric Morphism α (r : ring α) (K : field r) : ps_mul
  with signature eq_ps ==> eq_ps ==> eq_ps
  as ps_mul_morph.
Proof.
intros ps₁ ps₃ Heq₁ ps₂ ps₄ Heq₂.
rewrite ps_mul_compat_l; [ idtac | eassumption ].
rewrite ps_mul_compat_r; [ idtac | eassumption ].
reflexivity.
Qed.

Section other_theorems.

Variable α : Type.
Variable r : ring α.
Variable K : field r.

Theorem normalise_ps_eq : ∀ ps, (normalise_ps ps = ps)%ps.
Proof.
intros ps.
unfold normalise_ps.
unfold normalise_ps.
remember (series_order (ps_terms ps) 0) as n eqn:Hn .
symmetry in Hn.
destruct n as [n| ]; constructor.
 remember (greatest_series_x_power K (ps_terms ps) n) as x.
 remember (gcd_ps n x ps) as g eqn:Hg .
 pose proof (gcd_ps_is_pos n x ps) as Hgp; subst x.
 rewrite <- Hg in Hgp.
 unfold gcd_ps in Hg; simpl in Hg.
 remember (ps_ordnum ps + Z.of_nat n)%Z as x eqn:Hx .
 rewrite <- Z.gcd_assoc in Hg.
 remember (greatest_series_x_power K (ps_terms ps) n) as z.
 remember (Z.gcd (Zpos (ps_polydo ps)) (Z.of_nat z)) as y eqn:Hy ; subst z.
 rewrite ps_normal_adjust_eq with (k := Z.to_pos g) (n := n).
 unfold adjust_ps; simpl.
 unfold normalise_series.
 rewrite series_stretch_shrink.
  rewrite series_shift_left_shift; [ idtac | apply Hn ].
  rewrite <- positive_nat_Z.
  rewrite Pos2Nat_to_pos; [ idtac | assumption ].
  rewrite Z2Nat.id; [ idtac | apply Z.lt_le_incl; assumption ].
  rewrite Z.mul_comm.
  assert (x mod g = 0)%Z as Hxk.
   apply Z.mod_divide.
    intros H; revert Hgp; rewrite H; apply Z.lt_irrefl.

    rewrite Hg; apply Z.gcd_divide_l.

   apply Z.div_exact in Hxk.
    rewrite <- Hxk, Hx, Z.add_simpl_r.
    rewrite Hy, Z.gcd_comm, <- Z.gcd_assoc in Hg.
    remember (greatest_series_x_power K (ps_terms ps) n) as z.
    pose proof (Z.gcd_divide_l (Zpos (ps_polydo ps)) (Z.gcd (Z.of_nat z) x)) as Hgc.
    rewrite <- Hg in Hgc.
    destruct Hgc as (c, Hc).
    rewrite Hc.
    rewrite Z.div_mul.
     rewrite <- Z2Pos.inj_mul; [ idtac | idtac | assumption ].
      rewrite <- Hc; simpl.
      destruct ps; reflexivity.

      destruct c as [| c| c].
       exfalso; revert Hc; apply Pos2Z_ne_0.

       apply Pos2Z.is_pos.

       simpl in Hc.
       destruct g as [| g| g].
        exfalso; revert Hc; apply Pos2Z_ne_0.

        rewrite <- Pos2Z.opp_pos in Hc.
        apply Z.add_move_0_r in Hc.
        rewrite <- Pos2Z.inj_add in Hc.
        exfalso; revert Hc; apply Pos2Z_ne_0.

        apply Z.nle_gt in Hgp.
        exfalso; apply Hgp; apply Pos2Z.neg_is_nonpos.

     intros H; revert Hgp; rewrite H; apply Z.lt_irrefl.

    intros H1; revert Hgp; rewrite H1; apply Z.lt_irrefl.

  rewrite greatest_series_x_power_left_shift, Nat.add_0_r.
  rewrite Pos2Nat_to_pos; [ idtac | assumption ].
  remember (greatest_series_x_power K (ps_terms ps) n) as t.
  rewrite Hy in Hg.
  rewrite Z.gcd_assoc in Hg.
  remember (Z.gcd x (Zpos (ps_polydo ps))) as u.
  pose proof (Z.gcd_divide_r u (Z.of_nat t)) as H.
  rewrite <- Hg in H.
  destruct H as (c, Hc).
  exists (Z.to_nat c).
  rewrite <- Z2Nat.inj_mul.
   rewrite <- Hc.
   rewrite Nat2Z.id; symmetry; apply Heqt.

   apply Z.mul_le_mono_pos_r with (p := g); [ assumption | idtac ].
   rewrite <- Hc; simpl.
   apply Nat2Z.is_nonneg.

   apply Z.lt_le_incl; assumption.

 unfold normalise_ps; simpl.
 rewrite series_order_series_0, Hn.
 reflexivity.
Qed.

Theorem ps_ordnum_normalise : ∀ ps n p vn,
  series_order (ps_terms ps) 0 = fin n
  → p = greatest_series_x_power K (ps_terms ps) n
    → vn = (ps_ordnum ps + Z.of_nat n)%Z
      → ps_ordnum (normalise_ps ps) =
          (vn / Z.gcd vn (Z.gcd (Zpos (ps_polydo ps)) (Z.of_nat p)))%Z.
Proof.
intros ps n p vn Hn Hp Hvn.
unfold normalise_ps; simpl.
rewrite Hn; simpl.
rewrite <- Hp.
unfold gcd_ps; simpl.
rewrite <- Z.gcd_assoc.
rewrite <- Hvn.
reflexivity.
Qed.

Theorem ps_polydo_normalise : ∀ ps n p vn,
  series_order (ps_terms ps) 0 = fin n
  → p = greatest_series_x_power K (ps_terms ps) n
    → vn = (ps_ordnum ps + Z.of_nat n)%Z
      → ps_polydo (normalise_ps ps) =
        Z.to_pos
          (Zpos (ps_polydo ps) / Z.gcd (Zpos (ps_polydo ps)) (Z.gcd (Z.of_nat p) vn)).
Proof.
intros ps n p vn Hn Hp Hvn.
unfold normalise_ps; simpl.
rewrite Hn; simpl.
rewrite <- Hp.
unfold gcd_ps; simpl.
rewrite <- Z.gcd_assoc, Z.gcd_comm, <- Z.gcd_assoc.
rewrite <- Hvn.
reflexivity.
Qed.

Theorem ps_terms_normalise : ∀ ps n p vn,
  series_order (ps_terms ps) 0 = fin n
  → p = greatest_series_x_power K (ps_terms ps) n
    → vn = (ps_ordnum ps + Z.of_nat n)%Z
      → ps_terms (normalise_ps ps) =
        normalise_series n
          (Z.to_pos (Z.gcd vn (Z.gcd (Zpos (ps_polydo ps)) (Z.of_nat p))))
          (ps_terms ps).
Proof.
intros ps n p vn Hn Hp Hvn.
unfold normalise_ps; simpl.
rewrite Hn; simpl.
rewrite <- Hp.
unfold gcd_ps; simpl.
rewrite <- Z.gcd_assoc.
rewrite <- Hvn.
reflexivity.
Qed.

Theorem null_range_length_mul_add₂_distr_l : ∀ ps₁ ps₂ ps₃,
   series_order
     (ps_terms
        (adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃)%ps)) 0 =
   series_order
     (ps_terms
        (adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂)%ps (ps₁ * ps₃)%ps))) 0.
Proof.
intros ps₁ ps₂ ps₃; simpl.
unfold cm, cm_factor; simpl.
do 2 rewrite series_shift_0.
rewrite series_stretch_1.
remember (ps_ordnum ps₁) as v₁.
remember (ps_polydo ps₂) as c₂.
remember (ps_ordnum ps₂) as v₂.
remember (ps_polydo ps₁) as c₁.
remember (ps_ordnum ps₃) as v₃.
remember (ps_polydo ps₃) as c₃.
do 3 rewrite series_stretch_mul.
do 6 rewrite <- series_stretch_stretch.
rewrite series_stretch_add_distr.
do 2 rewrite stretch_shift_series_distr.
do 2 rewrite <- series_stretch_stretch.
symmetry.
rewrite series_mul_comm.
rewrite series_shift_mul.
rewrite series_add_comm.
rewrite series_mul_comm.
rewrite series_shift_mul.
rewrite series_add_comm.
replace (c₁ * c₃ * c₂)%positive with (c₁ * c₂ * c₃)%positive
 by apply Pos_mul_shuffle0.
rewrite <- series_mul_add_distr_r.
rewrite series_mul_comm.
do 2 rewrite Pos2Z.inj_mul, Z.mul_assoc.
do 4 rewrite Z.mul_add_distr_r.
remember (v₁ * Zpos c₂ * Zpos c₁ * Zpos c₃)%Z as x eqn:Hx .
replace (v₁ * Zpos c₃ * Zpos c₁ * Zpos c₂)%Z with x by (subst x; ring).
do 2 rewrite Z.add_min_distr_l.
do 2 rewrite Z.add_add_simpl_l_l.
clear x Hx.
do 2 rewrite <- Z2Nat_inj_mul_pos_r.
rewrite Pos2Z.inj_mul; do 2 rewrite Z.mul_assoc.
do 4 rewrite Z.mul_sub_distr_r.
rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ].
rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ].
rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ].
rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ].
rewrite Pos.mul_assoc.
do 2 f_equal.
f_equal.
 rewrite Pos_mul_shuffle0.
 do 2 f_equal.
 f_equal; [ ring | idtac ].
 f_equal; ring.

 rewrite Pos_mul_shuffle0.
 do 2 f_equal.
 f_equal; [ ring | idtac ].
 f_equal; ring.
Qed.

Theorem ps_ordnum_adjust_mul_add₂_distr_l : ∀ ps₁ ps₂ ps₃,
  ps_ordnum (adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃)%ps) =
  ps_ordnum (adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂)%ps (ps₁ * ps₃)%ps)).
Proof.
intros ps₁ ps₂ ps₃; simpl.
unfold cm; simpl.
unfold cm_factor.
f_equal.
rewrite Z.mul_1_r.
remember (ps_ordnum ps₁) as v₁.
remember (ps_polydo ps₂) as c₂.
remember (ps_ordnum ps₂) as v₂.
remember (ps_polydo ps₁) as c₁.
remember (ps_ordnum ps₃) as v₃.
remember (ps_polydo ps₃) as c₃.
do 3 rewrite Pos2Z.inj_mul.
do 3 rewrite Z.mul_assoc.
rewrite Z.mul_sub_distr_r.
do 3 rewrite <- positive_nat_Z.
do 5 rewrite Z.mul_add_distr_r.
rewrite Z.mul_sub_distr_r.
do 2 rewrite <- Nat2Z.inj_mul.
do 2 rewrite <- Z2Nat_inj_mul_pos_r.
do 2 rewrite Z.mul_sub_distr_r.
do 3 rewrite positive_nat_Z.
rewrite Z.add_sub_assoc.
f_equal.
 rewrite Z.mul_shuffle0.
 apply Z.add_cancel_l.
 rewrite <- Z.mul_assoc, Z.mul_shuffle0, Z.mul_assoc.
 reflexivity.

 do 2 f_equal.
 rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ].
 rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ].
 remember (v₁ * Zpos c₃ * Zpos c₁ * Zpos c₂)%Z as x.
 replace (v₁ * Zpos c₂ * Zpos c₁ * Zpos c₃)%Z with x by (subst; ring).
 rewrite Z.add_min_distr_l.
 rewrite Z.add_add_simpl_l_l.
 clear x Heqx.
 f_equal; [ ring | idtac ].
 f_equal; ring.
Qed.

Theorem ps_polydo_adjust_mul_add₂_distr_l : ∀ ps₁ ps₂ ps₃,
  ps_polydo (adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃)%ps) =
  ps_polydo (adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂)%ps (ps₁ * ps₃)%ps)).
Proof.
intros ps₁ ps₂ ps₃; simpl.
unfold cm; simpl.
unfold cm_factor.
rewrite Pos.mul_1_r.
do 2 rewrite Pos.mul_assoc.
rewrite Pos_mul_shuffle0.
reflexivity.
Qed.

Theorem ps_terms_adjust_mul_add₂_distr_l : ∀ ps₁ ps₂ ps₃,
  (ps_terms
     (adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃)%ps) =
   ps_terms
     (adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂)%ps (ps₁ * ps₃)%ps)))%ser.
Proof.
intros ps₁ ps₂ ps₃; simpl.
unfold cm; simpl.
unfold cm_factor.
do 2 rewrite series_shift_0.
rewrite series_stretch_1.
remember (ps_ordnum ps₁) as v₁.
remember (ps_polydo ps₂) as c₂.
remember (ps_ordnum ps₂) as v₂.
remember (ps_polydo ps₁) as c₁.
remember (ps_ordnum ps₃) as v₃.
remember (ps_polydo ps₃) as c₃.
do 3 rewrite series_stretch_mul.
do 6 rewrite <- series_stretch_stretch.
rewrite series_stretch_add_distr.
rewrite series_mul_add_distr_l.
symmetry.
rewrite series_mul_comm, series_shift_mul, series_mul_comm.
rewrite series_add_comm.
rewrite series_mul_comm, series_shift_mul, series_mul_comm.
do 2 rewrite Pos2Z.inj_mul.
do 2 rewrite Z.mul_assoc.
do 4 rewrite Z.mul_add_distr_r.
remember (v₁ * Zpos c₃ * Zpos c₁ * Zpos c₂)%Z as x.
replace (v₁ * Zpos c₂ * Zpos c₁ * Zpos c₃)%Z with x by (subst x; ring).
do 2 rewrite Z.add_min_distr_l.
do 2 rewrite Z.add_add_simpl_l_l.
clear x Heqx.
do 2 rewrite stretch_shift_series_distr.
do 2 rewrite <- Z2Nat_inj_mul_pos_r.
rewrite Pos2Z.inj_mul.
do 2 rewrite Z.mul_assoc.
do 4 rewrite Z.mul_sub_distr_r.
rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ].
rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ].
rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ].
rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ].
rewrite series_add_comm.
do 2 rewrite <- series_stretch_stretch.
rewrite Pos.mul_assoc.
rewrite Pos_mul_shuffle0.
remember (v₂ * Zpos c₁ * Zpos c₁ * Zpos c₃)%Z as x.
replace (v₂ * Zpos c₃ * Zpos c₁ * Zpos c₁)%Z with x by (subst; ring).
subst x.
remember (v₃ * Zpos c₁ * Zpos c₁ * Zpos c₂)%Z as x.
replace (v₃ * Zpos c₂ * Zpos c₁ * Zpos c₁)%Z with x by (subst; ring).
subst x.
remember (c₁ * c₃ * c₁)%positive as x.
rewrite Pos_mul_shuffle0 in Heqx.
subst x.
remember (c₁ * c₂ * c₁)%positive as x.
rewrite Pos_mul_shuffle0 in Heqx.
subst x.
reflexivity.
Qed.

Theorem ps_ordnum_adjust_normalise_mul_add₂_distr_l : ∀ ps₁ ps₂ ps₃ ps₄ ps₅ n,
  ps₄ = adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃)%ps
  → ps₅ = adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂)%ps (ps₁ * ps₃)%ps)
    → series_order (ps_terms ps₄) 0 = fin n
      → series_order (ps_terms ps₅) 0 = fin n
        → ps_ordnum (normalise_ps ps₄) = ps_ordnum (normalise_ps ps₅).
Proof.
intros ps₁ ps₂ ps₃ ps₄ ps₅ n Hps₄ Hps₅ Hn₄ Hn₅.
erewrite ps_ordnum_normalise; try reflexivity; try eassumption.
erewrite ps_ordnum_normalise; try reflexivity; try eassumption.
rewrite Hps₄, Hps₅.
rewrite ps_ordnum_adjust_mul_add₂_distr_l.
rewrite ps_polydo_adjust_mul_add₂_distr_l.
rewrite ps_terms_adjust_mul_add₂_distr_l.
reflexivity.
Qed.

Theorem ps_polydo_adjust_normalise_mul_add₂_distr_l : ∀ ps₁ ps₂ ps₃ ps₄ ps₅ n,
  ps₄ = adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃)%ps
  → ps₅ = adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂)%ps (ps₁ * ps₃)%ps)
    → series_order (ps_terms ps₄) 0 = fin n
      → series_order (ps_terms ps₅) 0 = fin n
        → ps_polydo (normalise_ps ps₄) = ps_polydo (normalise_ps ps₅).
Proof.
intros ps₁ ps₂ ps₃ ps₄ ps₅ n Hps₄ Hps₅ Hn₄ Hn₅.
erewrite ps_polydo_normalise; try reflexivity; try eassumption.
erewrite ps_polydo_normalise; try reflexivity; try eassumption.
rewrite Hps₄, Hps₅.
rewrite ps_ordnum_adjust_mul_add₂_distr_l.
rewrite ps_polydo_adjust_mul_add₂_distr_l.
rewrite ps_terms_adjust_mul_add₂_distr_l.
reflexivity.
Qed.

Theorem ps_terms_adjust_normalise_mul_add₂_distr_l : ∀ ps₁ ps₂ ps₃ ps₄ ps₅ n,
  ps₄ = adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃)%ps
  → ps₅ = adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂)%ps (ps₁ * ps₃)%ps)
    → series_order (ps_terms ps₄) 0 = fin n
      → series_order (ps_terms ps₅) 0 = fin n
        → (ps_terms (normalise_ps ps₄) = ps_terms (normalise_ps ps₅))%ser.
Proof.
intros ps₁ ps₂ ps₃ ps₄ ps₅ n Hps₄ Hps₅ Hn₄ Hn₅.
erewrite ps_terms_normalise; try reflexivity; try eassumption.
erewrite ps_terms_normalise; try reflexivity; try eassumption.
rewrite Hps₄, Hps₅.
rewrite ps_ordnum_adjust_mul_add₂_distr_l.
rewrite ps_polydo_adjust_mul_add₂_distr_l.
rewrite ps_terms_adjust_mul_add₂_distr_l.
reflexivity.
Qed.

Theorem ps_mul_add_distr_l : ∀ ps₁ ps₂ ps₃,
  (ps₁ * (ps₂ + ps₃) = ps₁ * ps₂ + ps₁ * ps₃)%ps.
Proof.
intros ips₁ ips₂ ips₃.
rewrite <- (normalise_ps_eq ips₁).
rewrite <- (normalise_ps_eq ips₂).
rewrite <- (normalise_ps_eq ips₃).
remember (normalise_ps ips₁) as ps₁ eqn:Hps₁ .
remember (normalise_ps ips₂) as ps₂ eqn:Hps₂ .
remember (normalise_ps ips₃) as ps₃ eqn:Hps₃ .
remember (ps_ordnum ps₁ * Zpos (ps_polydo ps₂) * Zpos (ps_polydo ps₃))%Z as vcc.
remember (Zpos (ps_polydo ps₁) * ps_ordnum ps₂ * Zpos (ps_polydo ps₃))%Z as cvc.
remember (Zpos (ps_polydo ps₁) * Zpos (ps_polydo ps₂) * ps_ordnum ps₃)%Z as ccv.
remember ((vcc + Z.min cvc ccv) * Zpos (ps_polydo ps₁))%Z as n₁.
remember ((vcc + Z.min cvc ccv) * Zpos (ps_polydo ps₁))%Z as n₂.
do 2 rewrite eq_ps_add_add₂.
rewrite ps_adjust_eq with (n := O) (k := ps_polydo ps₁); symmetry.
rewrite ps_adjust_eq with (n := O) (k := xH); symmetry.
remember (adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃))%ps as ps₄
 eqn:Hps₄ .
remember (adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂) (ps₁ * ps₃)))%ps as ps₅ eqn:Hps₅ .
remember (series_order (ps_terms ps₄) 0) as n₄ eqn:Hn₄ .
remember (series_order (ps_terms ps₅) 0) as n₅ eqn:Hn₅ .
symmetry in Hn₄, Hn₅.
assert (n₄ = n₅) as H by (subst; apply null_range_length_mul_add₂_distr_l).
move H at top; subst n₅.
destruct n₄ as [n₄| ].
 constructor; constructor; simpl.
  eapply ps_ordnum_adjust_normalise_mul_add₂_distr_l; eassumption.

  eapply ps_polydo_adjust_normalise_mul_add₂_distr_l; eassumption.

  eapply ps_terms_adjust_normalise_mul_add₂_distr_l; eassumption.

 rewrite ps_series_order_inf_iff in Hn₄.
 rewrite ps_series_order_inf_iff in Hn₅.
 rewrite Hn₄, Hn₅; reflexivity.
Qed.

Theorem ps_monom_add_l : ∀ c d n,
  (ps_monom (c + d)%K n = ps_monom c n + ps_monom d n)%ps.
Proof.
intros c d n.
unfold ps_monom; simpl.
rewrite ps_adjust_eq with (n := 0%nat) (k := Qden n).
unfold adjust_ps; simpl.
rewrite series_shift_0.
rewrite Z.sub_0_r.
apply mkps_morphism; simpl.
 constructor; intros i; simpl.
 rewrite Z.min_id; simpl.
 rewrite Z.sub_diag; simpl.
 rewrite Nat.sub_0_r.
 destruct (zerop (i mod Pos.to_nat (Qden n))) as [H| H].
  destruct (zerop (i / Pos.to_nat (Qden n))) as [H₁| H₁].
   reflexivity.

   rewrite rng_add_0_l; reflexivity.

  rewrite rng_add_0_l; reflexivity.

 unfold ps_ordnum_add; simpl.
 rewrite Z.min_id; reflexivity.

 unfold cm; simpl.
 reflexivity.
Qed.

Theorem ps_monom_mul : ∀ a b m n,
  (ps_monom a m * ps_monom b n = ps_monom (a * b)%K (m + n))%ps.
Proof.
intros a b m n.
progress unfold ps_mul; simpl.
unfold cm; simpl.
unfold ps_monom; simpl.
apply mkps_morphism; try reflexivity.
constructor; intros i; simpl.
unfold convol_mul; simpl.
destruct i; simpl.
 unfold summation; simpl.
 rewrite Nat.mod_0_l; [ idtac | apply Pos2Nat_ne_0 ].
 rewrite Nat.mod_0_l; [ simpl | apply Pos2Nat_ne_0 ].
 rewrite Nat.div_0_l; [ idtac | apply Pos2Nat_ne_0 ].
 rewrite Nat.div_0_l; [ idtac | apply Pos2Nat_ne_0 ].
 rewrite rng_add_0_r; reflexivity.

 rewrite all_0_summation_0; [ reflexivity | idtac ].
 intros j (_, Hj).
 rewrite fold_sub_succ_l.
 destruct (zerop (j mod Pos.to_nat (Qden n))) as [H₁| H₁].
  apply Nat.mod_divides in H₁; [ idtac | apply Pos2Nat_ne_0 ].
  destruct H₁ as (c, Hc).
  rewrite Nat.mul_comm in Hc; rewrite Hc.
  rewrite Nat.div_mul; [ idtac | apply Pos2Nat_ne_0 ].
  destruct (zerop c) as [H₁| H₁].
   subst c.
   rewrite Nat.mul_0_l, Nat.sub_0_r.
   destruct (zerop (S i mod Pos.to_nat (Qden m))) as [H₁| H₁].
    apply Nat.mod_divides in H₁; [ idtac | apply Pos2Nat_ne_0 ].
    destruct H₁ as (d, Hd).
    rewrite Nat.mul_comm in Hd; rewrite Hd.
    rewrite Nat.div_mul; [ idtac | apply Pos2Nat_ne_0 ].
    destruct (zerop d) as [H₁| H₁]; [ subst d; discriminate Hd | idtac ].
    rewrite rng_mul_0_r; reflexivity.

    rewrite rng_mul_0_r; reflexivity.

   rewrite rng_mul_0_l; reflexivity.

  rewrite rng_mul_0_l; reflexivity.
Qed.

Theorem ps_monom_mul_l : ∀ c d n,
  (ps_monom (c * d)%K n = ps_monom c 0 * ps_monom d n)%ps.
Proof.
intros c d n.
progress unfold ps_monom; simpl.
apply mkps_morphism; simpl; [ idtac | idtac | reflexivity ].
 constructor; intros i; simpl.
 destruct i; simpl.
  progress unfold convol_mul; simpl.
  rewrite summation_only_one; simpl.
  rewrite Nat.mod_0_l; auto with Arith; simpl.
  rewrite Nat.div_0_l; auto with Arith; simpl.

  progress unfold convol_mul; simpl.
  rewrite all_0_summation_0; [ reflexivity | idtac ].
  intros j (_, Hj).
  rewrite divmod_div.
  rewrite fold_sub_succ_l.
  rewrite Nat.div_1_r.
  destruct (zerop (j mod Pos.to_nat (Qden n))) as [H₁| H₁].
   apply Nat.mod_divides in H₁; auto with Arith.
   destruct H₁ as (e, He).
   rewrite Nat.mul_comm in He.
   rewrite He.
   rewrite Nat.div_mul; auto with Arith.
   destruct (zerop e) as [H₂| H₂].
    subst e; rewrite Nat.sub_0_r; simpl.
    rewrite rng_mul_0_r; reflexivity.

    rewrite rng_mul_0_l; reflexivity.

   rewrite rng_mul_0_l; reflexivity.

 rewrite Z.mul_1_r; reflexivity.
Qed.

Theorem ps_monom_add_r : ∀ c p q,
 (ps_monom c (p + q) = ps_monom c p * ps_monom 1%K q)%ps.
Proof.
intros c p q.
unfold ps_mul; simpl.
unfold cm; simpl.
unfold ps_monom; simpl.
apply mkps_morphism; try reflexivity.
unfold ps_mul; simpl.
unfold cm; simpl.
unfold ps_monom; simpl.
constructor; intros i; simpl.
unfold series_stretch; simpl.
unfold convol_mul; simpl.
destruct i; simpl.
 rewrite summation_only_one; simpl.
 rewrite Nat.mod_0_l; auto with Arith; simpl.
 rewrite Nat.mod_0_l; auto with Arith; simpl.
 rewrite Nat.div_0_l; auto with Arith; simpl.
 rewrite Nat.div_0_l; auto with Arith; simpl.
 rewrite rng_mul_1_r; reflexivity.

 rewrite all_0_summation_0; [ reflexivity | simpl ].
 intros j (_, Hj).
 destruct j; simpl.
  rewrite Nat.mod_0_l; auto with Arith; simpl.
  rewrite Nat.div_0_l; auto with Arith; simpl.
  destruct (zerop (S i mod Pos.to_nat (Qden p))) as [H| H].
   apply Nat.mod_divides in H; auto with Arith.
   destruct H as (d, Hd).
   rewrite Nat.mul_comm in Hd; rewrite Hd.
   rewrite Nat.div_mul; auto with Arith.
   destruct d; [ discriminate Hd | simpl ].
   rewrite rng_mul_0_r; reflexivity.

   rewrite rng_mul_0_r; reflexivity.

  destruct (zerop (S j mod Pos.to_nat (Qden q))) as [H| H].
   apply Nat.mod_divides in H; auto with Arith.
   destruct H as (d, Hd).
   rewrite Nat.mul_comm in Hd; rewrite Hd.
   rewrite Nat.div_mul; auto with Arith.
   destruct d; [ discriminate Hd | simpl ].
   rewrite rng_mul_0_l; reflexivity.

   rewrite rng_mul_0_l; reflexivity.
Qed.

End other_theorems.

author: roglo

repo: puiseuxth

save_path: github-repos/coq/roglo-puiseuxth


text:
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Data.HList.
Require Import ExtLib.Data.Option.
Require Import ExtLib.Data.Eq.
Require Import ExtLib.Tactics.
Require Import MirrorCore.SymI.
Require Import MirrorCore.ExprI.
Require Import MirrorCore.AbsAppI.
Require Import MirrorCore.Lambda.ExprCore.
Require Import MirrorCore.Lambda.ExprDI.

Set Implicit Arguments.
Set Strict Implicit.

Module ExprDenote <: ExprDenote.

  Section with_types.
    Context {typ : Set}.
    Context {func : Set}.
    Context {RType_typD : RType typ}.
    Context {Typ2_Fun : Typ2 _ RFun}.
    Context {RSym_func : RSym func}.

    (** Reasoning principles **)
    Context {RTypeOk_typD : RTypeOk}.
    Context {Typ2Ok_Fun : Typ2Ok Typ2_Fun}.
    Context {RSymOk_func : RSymOk RSym_func}.

    Let typ_arr : typ -> typ -> typ := @typ2 _ _ _ _.
    Let arr_match := @typ2_match _ _ _ _.
    Let typD_arr
    : forall a b, typD (typ_arr a b) = (typD a -> typD b)
      := @typ2_cast _ _ _ _.

    Definition Rcast T {a b} (pf : Rty a b) : T (typD a) -> T (typD b) :=
      Relim T (Rsym pf).

    Definition Rcast_val
    : forall {a b} (pf : Rty a b), typD a -> typD b :=
      @Rcast (fun T => T).

    Global Arguments Rcast_val [_ _] !pf _ /.  (* COMPAT(8.5): To be fixed in 8.6 *)
    Global Arguments Rcast _ [_ _] !pf _ /.  (* COMPAT(8.5): To be fixed in 8.6 *)

    Section exprT.
      Variables tus tvs : tenv typ.

      (** Auxiliary definitions **)
      Definition exprT_GetUAs (n : nat) (t : typ) :
        option (exprT tus tvs (typD t)) :=
        match nth_error_get_hlist_nth typD tus n with
        | Some (existT _ t' get) =>
          match type_cast t' t with
          | Some cast => Some (fun us vs => Rcast_val cast (get us))
          | _ => None
          end
        | _ => None
        end.

      Definition exprT_GetVAs (n : nat) (t : typ) :
        option (exprT tus tvs (typD t)) :=
        match nth_error_get_hlist_nth typD tvs n with
        | Some (existT _ t' get) =>
          match type_cast t' t with
          | Some cast => Some (fun us vs => Rcast_val cast (get vs))
          | _ => None
          end
        | _ => None
        end.

    End exprT.

    Definition func_simul (f : func) : option { t : typ & typD t } :=
      match typeof_sym f as Z
            return Z = typeof_sym (RSym:=RSym_func) f -> option _
      with
        | None => fun _ => None
        | Some T => fun pf =>
          Some (@existT _ _ T
                        (match pf in _ = Z
                               return match Z with
                                      | Some t => typD t
                                      | None => unit:Type
                                      end -> typD _
                         with
                         | eq_refl => fun x => x
                         end (symD f)))
      end eq_refl.

    Section lambda_exprD.
      Variable tus : tenv typ.

      Fixpoint lambda_exprD (tvs : tenv typ) (t : typ) (e : expr typ func)
      : option (exprT tus tvs (typD t)) :=
        match e return option (exprT tus tvs (typD t)) with
          | Var v => @exprT_GetVAs tus tvs v t
          | Inj f =>
            match @symAs _ _ _ _ f t with
              | None => None
              | Some val =>
                Some (exprT_Inj tus tvs val)
            end
          | App f x =>
            match lambda_exprD_simul tvs x with
              | None => None
              | Some (existT _ t' x) =>
                match lambda_exprD tvs (typ_arr t' t) f with
                  | None => None
                  | Some f => Some (exprT_App f x)
                end
            end
          | Abs t' e =>
            arr_match (fun T => option (exprT tus tvs T)) t
                      (fun d r =>
                         match type_cast d t' with
                           | None => None
                           | Some cast =>
                             match lambda_exprD (t' :: tvs) r e with
                               | None => None
                               | Some val =>
                                 Some (fun us vs x =>
                                         val us (Hcons (Rcast_val cast x) vs))
                             end
                         end)
                      None
          | UVar u => @exprT_GetUAs tus tvs u t
        end
      with lambda_exprD_simul (tvs : tenv typ) (e : expr typ func)
      : option { t : typ & exprT tus tvs (typD t) } :=
        match e return option { t : typ & exprT tus tvs (typD t) } with
          | Var v => exprT_UseV tus tvs v
          | Inj f =>
            match @func_simul f with
              | None => None
              | Some (existT _ t val) =>
                Some (@existT _ (fun t => exprT tus tvs (typD t))
                              t (fun _ _ => val))
            end
          | App f x =>
            match lambda_exprD_simul tvs f with
              | None => None
              | Some (existT _ t' f) =>
                arr_match (fun T =>
                             exprT tus tvs T ->
                             option { t : typ & exprT tus tvs (typD t) })
                          t'
                          (fun d r f =>
                             match lambda_exprD tvs d x with
                               | None => None
                               | Some x =>
                                 Some (@existT _
                                               (fun t => exprT tus tvs (typD t))
                                               r
                                               (fun us vs => (f us vs) (x us vs)))
                             end)
                          (fun _ => None)
                          f
            end
          | Abs t e =>
            match lambda_exprD_simul (t :: tvs) e with
              | None => None
              | Some (existT _ t' f) =>
                Some (@existT _ (fun t => exprT tus tvs (typD t))
                              (typ_arr t t')
                              match eq_sym (typD_arr t t') in _ = T
                                    return exprT tus tvs T
                              with
                                | eq_refl => fun us vs x => f us (Hcons x vs)
                              end)
            end
          | UVar u => exprT_UseU tus tvs u
        end.
    End lambda_exprD.

    Section typeof_expr.
      Variable tus : tenv typ.

      Definition type_of_apply (tv x : typ) : option typ :=
        arr_match (fun _ => option typ) tv
                  (fun d r =>
                     match type_cast d x with
                       | Some _ => Some r
                       | None => None
                     end)
                  None.

      Fixpoint typeof_expr (tvs : tenv typ) (e : expr typ func)
      : option typ :=
        match e with
        | Var x  => nth_error tvs x
        | UVar x => nth_error tus x
        | Inj f => typeof_sym f
        | App e e' =>
          match typeof_expr tvs e
              , typeof_expr tvs e'
          with
            | Some tf , Some tx =>
              type_of_apply tf tx
            | _ , _ => None
          end
        | Abs t e =>
          match typeof_expr (t :: tvs) e with
            | None => None
            | Some t' => Some (typ_arr t t')
          end
      end.
    End typeof_expr.

    (** Equations **)
    Theorem lambda_exprD_Var
    : RTypeOk -> Typ2Ok Typ2_Fun -> RSymOk RSym_func ->
      forall tus tvs t v,
        lambda_exprD tus tvs t (Var v) =
        match nth_error_get_hlist_nth typD tvs v with
        | Some (existT _ t' get) =>
          match type_cast t' t with
          | Some cast => Some (fun us vs => Rcast_val cast (get vs))
          | _ => None
          end
        | _ => None
        end.
    Proof. reflexivity. Qed.

    Theorem lambda_exprD_UVar
    : RTypeOk -> Typ2Ok Typ2_Fun -> RSymOk RSym_func ->
      forall tus tvs t u,
        lambda_exprD tus tvs t (UVar u) =
        match nth_error_get_hlist_nth typD tus u with
        | Some (existT _ t' get) =>
          match type_cast t' t with
          | Some cast => Some (fun us vs => Rcast_val cast (get us))
          | _ => None
          end
        | _ => None
        end.
    Proof. reflexivity. Qed.

    Theorem lambda_exprD_Inj
    : RTypeOk -> Typ2Ok Typ2_Fun -> RSymOk RSym_func ->
      forall tus tvs t s,
        lambda_exprD tus tvs t (Inj s) =
        match symAs s t with
        | Some val => Some (fun _ _ => val)
        | _ => None
        end.
    Proof. reflexivity. Qed.

    Lemma lambda_exprD_App'
    : forall tus tvs t f x,
        lambda_exprD tus tvs t (App f x) =
        match lambda_exprD_simul tus tvs x with
        | Some (existT _ t' x) =>
          match lambda_exprD tus tvs (typ_arr t' t) f with
          | Some f => Some (exprT_App f x)
          | _ => None
          end
        | _ => None
        end.
    Proof. reflexivity. Qed.

    Lemma lambda_exprD_simul_App'
    : forall tus tvs f x,
        lambda_exprD_simul tus tvs (App f x) =
        match lambda_exprD_simul tus tvs f with
        | Some (existT _ t' f) =>
          arr_match (fun T =>
                       exprT tus tvs T ->
                       option { t : typ & exprT tus tvs (typD t) })
                    t'
                    (fun d r f =>
                       match lambda_exprD tus tvs d x with
                       | Some x =>
                         Some (@existT _
                                       (fun t => exprT tus tvs (typD t))
                                       r
                                       (fun us vs => (f us vs) (x us vs)))
                       | _ => None
                       end)
                    (fun _ => None)
                    f
        | _ => None
        end.
    Proof. reflexivity. Qed.

    Lemma lambda_exprD_Abs'
    : forall tus e tvs t' t,
        lambda_exprD tus tvs t (Abs t' e) =
        arr_match (fun T => option (exprT tus tvs T)) t
                  (fun d r =>
                     match type_cast d t'
                         , lambda_exprD tus (t' :: tvs) r e
                     with
                     | Some cast , Some val =>
                       Some (fun us vs x =>
                               val us (Hcons (Rcast_val cast x) vs))
                     | _ , _ => None
                     end)
                  None.
    Proof. reflexivity. Qed.

    Lemma lambda_exprD_simul_Abs'
    : forall tus e tvs t,
        lambda_exprD_simul tus tvs (Abs t e) =
        match lambda_exprD_simul tus (t :: tvs) e with
        | Some (existT _ t' f) =>
          Some (@existT _ (fun t => exprT tus tvs (typD t))
                        (typ_arr t t')
                        match eq_sym (typD_arr t t') in _ = T
                              return exprT tus tvs T
                        with
                        | eq_refl => fun us vs x => f us (Hcons x vs)
                        end)
        | _ => None
        end.
    Proof. reflexivity. Qed.

    Theorem lambda_exprD_Abs
    : RTypeOk -> Typ2Ok Typ2_Fun -> RSymOk RSym_func ->
      forall tus tvs t t' e,
        lambda_exprD tus tvs t (Abs t' e) =
        arr_match (fun T => option (exprT tus tvs T)) t
                  (fun d r =>
                     match type_cast d t'
                         , lambda_exprD tus (t' :: tvs) r e
                     with
                     | Some cast , Some val =>
                       Some (fun us vs x =>
                               val us (Hcons (Rcast_val cast x) vs))
                     | _ , _ => None
                     end)
                  None.
    Proof. reflexivity. Qed.

    Lemma lambda_exprD_typeof_expr
    : forall tus e tvs t val,
        lambda_exprD tus tvs t e = Some val \/
        lambda_exprD_simul tus tvs e = Some (@existT _ _ t val) ->
        typeof_expr tus tvs e = Some t.
    Proof.
      induction e; simpl; intros.
      { unfold lambda_exprD, lambda_exprD_simul, exprT_GetVAs, exprT_UseV in *. simpl in *.
        destruct H; forward; inv_all; subst;
        eapply nth_error_get_hlist_nth_Some in H0; destruct H0; simpl in *; auto.
        red in r. subst. auto. }
      { unfold lambda_exprD, lambda_exprD_simul, func_simul, symAs in *; simpl in *.
        generalize dependent (symD f).
        destruct (typeof_sym f).
        { destruct 1. forward. inv_all; subst. auto. }
        { destruct 2; congruence. } }
      { rewrite lambda_exprD_App', lambda_exprD_simul_App' in H; simpl in H.
        destruct H; forward; inv_all; subst.
        { specialize (IHe1 _ _ _ (or_introl H1)).
          specialize (IHe2 _ _ _ (or_intror H0)).
          Cases.rewrite_all_goal.
          unfold type_of_apply.
          unfold arr_match. rewrite typ2_match_iota; eauto.
          rewrite type_cast_refl; eauto.
          rewrite eq_Const_eq. reflexivity. }
        { destruct (typ2_match_case x).
          { destruct H as [ ? [ ? [ ? ? ] ] ].
            rewrite H in *.
            specialize (IHe1 _ _ _ (or_intror H0)).
            red in x2. subst. simpl in *.
            Require Import MirrorCore.Util.Compat.
            autorewrite_with_eq_rw_in H1.
            forward. inv_all; subst.
            specialize (IHe2 _ _ _ (or_introl _ H1)).
            rewrite IHe2. subst.
            unfold type_of_apply. rewrite H.
            rewrite type_cast_refl; eauto. simpl. revert H2.
            do 2 rewrite eq_Const_eq.
            intro. inv_all. subst.
            reflexivity. }
          { rewrite H in *. congruence. } } }
      { rewrite lambda_exprD_simul_Abs', lambda_exprD_Abs in H; eauto; destruct H.
        { destruct (typ2_match_case t0).
          { destruct H0 as [ ? [ ? [ ? ? ] ] ].
            rewrite H0 in *.
            red in x1. subst. simpl in *.
            consider (lambda_exprD tus (t :: tvs) x0 e); intros.
            { specialize (IHe _ _ _ (or_introl H)).
              rewrite IHe.
              consider (type_cast x t); intros.
              { red in r. subst; auto. }
              { exfalso. clear - H2.
                destruct (eq_sym (typ2_cast x x0)).
                congruence. } }
            { exfalso. clear - H1. destruct (eq_sym (typ2_cast x x0)).
              destruct (type_cast x t); congruence. } }
          { rewrite H0 in H. congruence. } }
        { simpl in *. forward.
          specialize (IHe _ _ _ (or_intror H0)).
          rewrite IHe. inv_all; subst. auto. } }
      { unfold lambda_exprD_simul, lambda_exprD, exprT_GetUAs, exprT_UseU in *. simpl in *.
        destruct H; forward; inv_all; subst;
        eapply nth_error_get_hlist_nth_Some in H0; destruct H0; auto.
        red in r. subst. auto. }
    Qed.

    Lemma lambda_exprD_deterministic
    : forall tus e tvs t1 t2 val val',
        lambda_exprD tus tvs t1 e = Some val ->
        lambda_exprD tus tvs t2 e = Some val' ->
        Rty t1 t2.
    Proof.
      induction e; simpl; intros; red.
      { unfold lambda_exprD, exprT_GetVAs in *. simpl in *.
        forward; inv_all; subst. }
      { unfold lambda_exprD in *; simpl in *. forward; inv_all; subst.
        unfold symAs in *.
        generalize dependent (symD f).
        destruct (typeof_sym f); intros; try congruence.
        forward. }
      { rewrite lambda_exprD_App' in *. simpl in *.
        forward. inv_all; subst.
        specialize (IHe1 _ _ _ _ _ H2 H1).
        eapply typ2_inj in IHe1; eauto. destruct IHe1.
        destruct H3. reflexivity. }
      { rewrite lambda_exprD_Abs in *; eauto.
        destruct (typ2_match_case t1).
        { destruct (typ2_match_case t2).
          { forward_reason. unfold Rty in *.
            rewrite H2 in *. subst. simpl in *.
            rewrite H1 in *. clear H2 H1.
            repeat match goal with
                     | H : match ?X with eq_refl => None end = Some _ |- _ =>
                       exfalso; clear - H; destruct X; congruence
                     | H : context [ match ?X with _ => _ end ] |- _ =>
                       consider X; intros
                   end; subst.
            specialize (IHe _ _ _ _ _ H1 H3).
            red in r; red in r0.
            subst. reflexivity. }
          { rewrite H2 in *; congruence. } }
        { rewrite H1 in *. congruence. } }
      { unfold lambda_exprD, exprT_GetUAs in *. simpl in *.
        forward; inv_all; subst. }
    Qed.

    (** NOTE: These are requiring decidable equality **)
    Local Instance RelDec_eq_typ : RelDec (@eq typ) := RelDec_Rty _.
    Local Instance RelDecCorrect_eq_typ : RelDec_Correct RelDec_eq_typ :=
      _.

    Lemma exprD_simul'
    : forall tus e tvs tv,
        lambda_exprD_simul tus tvs e = Some tv <->
        (typeof_expr tus tvs e = Some (projT1 tv) /\
         lambda_exprD tus tvs (projT1 tv) e = Some (projT2 tv)).
    Proof.
      induction e; simpl.
      { unfold lambda_exprD_simul, lambda_exprD, exprT_UseV, exprT_GetVAs. simpl. intros.
        forward; inv_all; subst; simpl.
        eapply nth_error_get_hlist_nth_Some in H0. simpl in *.
        destruct H0.
        rewrite x0. destruct tv. simpl in *.
        split; intros.
        { inv_all. subst. rewrite type_cast_refl; eauto. subst; auto. }
        { destruct H0. inv_all; subst.
          rewrite type_cast_refl in H1; eauto. inv_all; subst.
          eauto. } }
      { unfold lambda_exprD, lambda_exprD_simul,func_simul, symAs. simpl in *; intros.
        generalize (symD f).
        destruct (typeof_sym f).
        { split; intros; forward; inv_all; subst; simpl.
          { rewrite type_cast_refl; eauto. }
          { red in r. subst. destruct H0. destruct tv.
            simpl in *; forward; inv_all; subst.
            reflexivity. } }
        { intuition congruence. } }
      { intros. specialize (@IHe1 tvs).
        specialize (IHe2 tvs).
        rewrite lambda_exprD_App'. rewrite lambda_exprD_simul_App'.
        simpl in *.
        split; intros.
        { forward; inv_all; subst; simpl.
          specialize (proj1 (IHe1 _) eq_refl); clear IHe1.
          intros. forward_reason.
          Cases.rewrite_all_goal. simpl in *.
          destruct (typ2_match_case x).
          { destruct H3 as [ ? [ ? [ ? ? ] ] ].
            unfold type_of_apply.
            unfold Rty in *. subst. simpl in *.
            rewrite H3 in H1.
            destruct tv; simpl in *.
            consider (lambda_exprD_simul tus tvs e2); intros.
            { destruct s. specialize (proj1 (IHe2 _) eq_refl); clear IHe2.
              simpl in *. intros. forward_reason.
              Cases.rewrite_all_goal. simpl in *.
              consider (lambda_exprD tus tvs x0 e2).
              { intros.
                unfold exprT_App in *. clear H3.
                specialize (lambda_exprD_deterministic _ _ _ H1 H6).
                unfold Rty. intros; subst.
                assert (x1 = x).
                { clear - H7. destruct (eq_sym (typ2_cast x2 x1)).
                  inv_all. auto. }
                subst. Cases.rewrite_all_goal.
                rewrite type_cast_refl; eauto.
                split.
                { rewrite eq_Const_eq in *. reflexivity. }
                { unfold typ_arr. rewrite H2.
                  autorewrite_with_eq_rw_in H7.
                  autorewrite_with_eq_rw.
                  rewrite H6 in H1.
                  inv_all. subst. reflexivity. } }
              { intros. exfalso. clear - H7.
                destruct (eq_sym (typ2_cast x0 x1)).
                congruence. } }
            { exfalso.
              autorewrite_with_eq_rw_in H1.
              forward. inv_all. subst. subst.
              specialize (H5 (@existT _ _ x0 e3)); simpl in *.
              rewrite H1 in *.
              erewrite lambda_exprD_typeof_expr in H5.
              2: eauto.
              autorewrite_with_eq_rw_in H6.
              destruct H5.
              assert (Some x0 = Some x0 /\ Some e3 = Some e3); auto.
              apply H7 in H8. congruence. } }
          { rewrite H3 in H1. congruence. } }
        { destruct H. forward; inv_all; subst.
          specialize (proj1 (IHe2 _) eq_refl); clear IHe2.
          intros; forward_reason; inv_all; subst; simpl in *.
          unfold type_of_apply in *.
          destruct (typ2_match_case t).
          { destruct H0 as [ ? [ ? [ ? ? ] ] ].
            rewrite H0 in H5.
            red in x2. subst; simpl in *.
            rewrite eq_Const_eq in H5. forward.
            red in r. inv_all; subst.
            destruct tv; simpl in *.
            specialize (IHe1 (@existT _ _ (typ_arr x x0) e0)).
            simpl in *. destruct IHe1. forward_reason.
            rewrite H8. rewrite H0.
            autorewrite_with_eq_rw.
            Cases.rewrite_all_goal. f_equal. f_equal. subst.
            unfold exprT_App. clear.
            generalize (typ2_cast x x0). intro.
            unfold typ_arr in *.
            generalize dependent (typD (typ2 x x0)).
            intros. revert e0. clear. subst. auto. }
          { rewrite H0 in H5. congruence. } } }
      { intros. rewrite lambda_exprD_Abs, lambda_exprD_simul_Abs'; eauto.
        unfold typ_arr, arr_match in *.
        simpl; split; intros; forward; inv_all; subst; simpl in *.
        { eapply IHe in H0. forward_reason. simpl in *.
          Cases.rewrite_all_goal. split; auto.
          rewrite typ2_match_iota; auto.
          rewrite type_cast_refl; eauto.
          Cases.rewrite_all_goal.
          unfold Rcast_val.
          rewrite eq_option_eq. reflexivity. }
        { forward_reason; inv_all; subst.
          destruct tv; simpl in *; subst.
          rewrite typ2_match_iota in H1; eauto.
          rewrite type_cast_refl in *; eauto.
          specialize (IHe (t :: tvs)).
          consider (lambda_exprD tus (t :: tvs) t0 e).
          { intros.
            rewrite eq_option_eq in H1. inv_all; subst.
            specialize (IHe (@existT _ _ t0 e1)).
            simpl in *. destruct IHe; forward_reason.
            Cases.rewrite_all_goal.
            unfold Rcast_val. reflexivity. }
          { intros. exfalso. clear - H1.
            destruct (eq_sym (typ2_cast t t0)). congruence. } } }
      { unfold lambda_exprD, lambda_exprD_simul, exprT_UseU, exprT_GetUAs. simpl. intros.
        forward; inv_all; subst; simpl.
        eapply nth_error_get_hlist_nth_Some in H0. simpl in *.
        destruct H0.
        rewrite x0. destruct tv. simpl in *.
        split; intros.
        { inv_all. subst. rewrite type_cast_refl; eauto. subst; auto. }
        { destruct H0. inv_all; subst.
          rewrite type_cast_refl in H1; eauto. inv_all; subst.
          reflexivity. } }
    Qed.

    Theorem lambda_exprD_App
    : (* RTypeOk _ -> Typ2Ok Typ2_Fun -> RSymOk RSym_func -> *)
      forall tus tvs t f x,
        lambda_exprD tus tvs t (App f x) =
        match typeof_expr tus tvs x with
        | Some t' =>
          match lambda_exprD tus tvs (typ_arr t' t) f
              , lambda_exprD tus tvs t' x
          with
          | Some f , Some x => Some (exprT_App f x)
          | _ , _ => None
          end
        | _ => None
        end.
    Proof.
      simpl. intros.
      rewrite lambda_exprD_App'. simpl.
      consider (lambda_exprD_simul tus tvs x); intros.
      { destruct s.
        generalize (@lambda_exprD_typeof_expr tus x tvs _ _ (or_intror H)).
        intros. rewrite H0.
        forward.
        eapply exprD_simul' in H.
        simpl in *. destruct H.
        rewrite H2. reflexivity. }
      { consider (typeof_expr tus tvs x); auto; intros.
        consider (lambda_exprD tus tvs (typ_arr t0 t) f); auto; intros.
        consider (lambda_exprD tus tvs t0 x); auto; intros.
        exfalso.
        assert (lambda_exprD_simul tus tvs x = Some (@existT _ _ t0 e0)).
        rewrite exprD_simul'. split; auto.
        congruence. }
    Qed.

    Theorem lambda_exprD_respects
    : RTypeOk -> Typ2Ok Typ2_Fun -> RSymOk RSym_func ->
      forall tus tvs t t' e (pf : Rty t' t),
        lambda_exprD tus tvs t e =
        Rcast (fun T => option (exprT tus tvs T)) pf
              (lambda_exprD tus tvs t' e).
    Proof.
      destruct pf. change (eq_refl t') with (Rrefl t').
      unfold Rcast. rewrite Relim_refl; eauto with typeclass_instances.
    Qed.

  End with_types.

End ExprDenote.

author: gmalecha

repo: mirror-core

save_path: github-repos/coq/gmalecha-mirror-core


text:
Require Import VST.veric.juicy_base.
Require Import VST.veric.juicy_mem VST.veric.juicy_mem_lemmas VST.veric.juicy_mem_ops.
Require Import VST.veric.res_predicates.
Require Import VST.veric.extend_tc.
Require Import VST.veric.Clight_seplog.
Require Import VST.veric.Clight_assert_lemmas.
Require Import VST.veric.Clight_core.
Require Import VST.sepcomp.extspec.
Require Import VST.sepcomp.step_lemmas.
Require Import VST.veric.tycontext.
Require Import VST.veric.expr2.
Require Import VST.veric.expr_lemmas.
Require Import VST.veric.juicy_extspec.
Require Import VST.veric.semax.
Require Import VST.veric.semax_lemmas.
Require Import VST.veric.Clight_lemmas.
Require Import VST.veric.own.

Local Open Scope pred.

(* This file contains two parts:
   1. Proof of semax_conseq.
   2. Deriving simpler and older version of consequence rules from semax_conseq.
   3. semax_extract_pre, and proof of semax_adapt_frame rules from semax_conseq, and 2 specializations of semax_adapt_frame. *)

(* Part 1: Proof of semax_conseq *)

Lemma _guard_mono: forall Espec ge Delta f (P Q: assert) k,
  (forall rho, P rho |-- Q rho) ->
  _guard Espec ge Delta f Q k |-- _guard Espec ge Delta f P k.
Proof.
  intros.
  unfold _guard.
  apply allp_derives; intros tx.
  apply allp_derives; intros vx.
  apply fash_derives.
  apply imp_derives; auto.
Qed.

Lemma guard_mono: forall Espec ge Delta f (P Q: assert) k,
  (forall rho, P rho |-- Q rho) ->
  guard Espec ge Delta f Q k |-- guard Espec ge Delta f P k.
Proof.
  intros.
  unfold guard.
  apply _guard_mono; auto.
Qed.

Lemma rguard_mono: forall Espec ge Delta f (P Q: ret_assert) k,
  (forall rk vl rho, proj_ret_assert P rk vl rho |-- proj_ret_assert Q rk vl rho) ->
  rguard Espec ge Delta f Q k |-- rguard Espec ge Delta f P k.
Proof.
  intros.
  unfold rguard.
  apply allp_derives; intros ek.
  apply allp_derives; intros vl.
  apply _guard_mono; auto.
Qed.

Definition fupd_ret_assert (Q: ret_assert): ret_assert :=
          {| RA_normal := fun rho => fupd (RA_normal Q rho);
             RA_break := fun rho => fupd (RA_break Q rho);
             RA_continue := fun rho => fupd (RA_continue Q rho);
             RA_return := fun v rho => RA_return Q v rho |}.
(* Asymmetric consequence: since there's no CompCert step that
   corresponds to RA_return, we can't do an update there. We could
   probably add a bupd if we really want to, but it may not be
   necessary. *)

Lemma fupd_fupd_andp_prop : forall P Q, fupd (!! P && fupd Q) = fupd (!!P && Q).
Proof.
  intros; apply pred_ext.
  - eapply derives_trans, fupd.fupd_trans.
    apply fupd.fupd_mono, fupd.fupd_andp_prop.
  - apply fupd.fupd_mono.
    apply andp_derives, fupd.fupd_intro; auto.
Qed.

Lemma fupd_idem : forall P, fupd (fupd P) = fupd P.
Proof.
  intros; apply pred_ext.
  - apply fupd.fupd_trans.
  - apply fupd.fupd_intro.
Qed.

Lemma proj_fupd_ret_assert: forall Q ek vl rho,
  fupd (proj_ret_assert (fupd_ret_assert Q) ek vl rho) = fupd (proj_ret_assert Q ek vl rho).
Proof.
  intros.
  destruct ek; simpl; auto; apply fupd_fupd_andp_prop.
Qed.

(* The following four lemmas is not now used. but after deep embedded hoare logic (SL_as_Logic) is
ported, the frame does not need to be quantified in the semantic definition of semax. Then,
these two lemmas can replace the other two afterwards. *)

Lemma assert_safe_fupd':
  forall {Espec: OracleKind} gx vx tx rho (P: environ -> pred rmap) Delta f k,
    match k with Ret _ _ => False | _ => True end ->
    let PP1 := !! guard_environ Delta f rho in
    let PP2 := funassert Delta rho in
    PP1 && (P rho) && PP2 >=>
    assert_safe Espec gx f vx tx k rho =
    PP1 && (fupd (P rho)) && PP2 >=>
    assert_safe Espec gx f vx tx k rho.
Proof.
  intros.
  apply pred_ext.
  * eapply derives_trans; [apply fupd.subp_fupd, derives_refl | apply subp_derives, assert_safe_fupd; auto].
    eapply derives_trans; [apply andp_derives, derives_refl; apply fupd.fupd_andp_prop|].
    rewrite andp_comm, (andp_comm (_ && _)).
    apply fupd.fupd_andp_corable, corable_funassert.
  * apply subp_derives, derives_refl.
    apply andp_derives, derives_refl.
    apply andp_derives, fupd.fupd_intro; apply derives_refl.
Qed.

Lemma _guard_fupd':
  forall {Espec: OracleKind} ge Delta (P: environ -> pred rmap) f k,
    match k with Ret _ _ => False | _ => True end ->
    _guard Espec ge Delta f P k = _guard Espec ge Delta f (fun rho => fupd (P rho)) k.
Proof.
  intros.
  unfold _guard.
  f_equal; extensionality tx.
  f_equal; extensionality vx.
  apply assert_safe_fupd'; auto.
Qed.

Lemma guard_fupd':
  forall {Espec: OracleKind} ge Delta f (P: environ -> pred rmap) k,
    guard Espec ge Delta f P k = guard Espec ge Delta f (fun rho => fupd (P rho)) k.
Proof.
  intros.
  apply _guard_fupd'; auto.
Qed.

Lemma exit_cont_nonret : forall ek vl k, ek <> EK_return ->
  match exit_cont ek vl k with Ret _ _ => False | _ => True end.
Proof.
  destruct ek; try contradiction; intros; simpl.
  - destruct vl; auto.
  - induction k; simpl; auto.
  - induction k; simpl; auto.
Qed.

Lemma rguard_fupd':
  forall {Espec: OracleKind} ge Delta f (P: ret_assert) k,
    rguard Espec ge Delta f P k = rguard Espec ge Delta f (fupd_ret_assert P) k.
Proof.
  intros.
  unfold rguard.
  f_equal; extensionality ek.
  f_equal; extensionality vl.
  destruct (eq_dec ek EK_return); subst; auto.
  rewrite _guard_fupd'; [|apply exit_cont_nonret; auto].
  setoid_rewrite _guard_fupd' at 2; [|apply exit_cont_nonret; auto].
  apply pred_ext; apply _guard_mono; intros; rewrite proj_fupd_ret_assert; auto.
Qed.

Lemma assert_safe_fupd:
  forall {Espec: OracleKind} gx vx tx rho (F P: environ -> pred rmap) Delta f k,
    match k with Ret _ _ => False | _ => True end ->
    let PP1 := !! guard_environ Delta f rho in
    let PP2 := funassert Delta rho in
    PP1 && (F rho * P rho) && PP2 >=>
    assert_safe Espec gx f vx tx k rho =
    PP1 && (F rho * fupd (P rho)) && PP2 >=>
    assert_safe Espec gx f vx tx k rho.
Proof.
  intros.
  apply pred_ext.
  + eapply derives_trans; [apply fupd.subp_fupd, derives_refl | apply subp_derives, assert_safe_fupd; auto].
    eapply derives_trans; [apply andp_derives, derives_refl; apply andp_derives, fupd.fupd_frame_l; apply derives_refl|].
    eapply derives_trans; [apply andp_derives, derives_refl; apply fupd.fupd_andp_prop|].
    rewrite andp_comm, (andp_comm (_ && _)).
    apply fupd.fupd_andp_corable, corable_funassert.
  + apply subp_derives, derives_refl.
    apply andp_derives, derives_refl.
    apply andp_derives, sepcon_derives, fupd.fupd_intro; apply derives_refl.
Qed.

Lemma _guard_fupd:
  forall {Espec: OracleKind} ge Delta f (F P: environ -> pred rmap) k,
    match k with Ret _ _ => False | _ => True end ->
    _guard Espec ge Delta f (fun rho => F rho * P rho) k = _guard Espec ge Delta f (fun rho => F rho * fupd (P rho)) k.
Proof.
  intros.
  unfold _guard.
  f_equal; extensionality tx.
  f_equal; extensionality vx.
  apply assert_safe_fupd; auto.
Qed.

Lemma guard_fupd:
  forall {Espec: OracleKind} ge Delta f (F P: environ -> pred rmap) k,
    guard Espec ge Delta f (fun rho => F rho * P rho) k = guard Espec ge Delta f (fun rho => F rho * fupd (P rho)) k.
Proof.
  intros.
  apply _guard_fupd; auto.
Qed.

Lemma fupd_fupd_frame_l : forall P Q, fupd (P * fupd Q) = fupd (P * Q).
Proof.
  intros; apply pred_ext.
  - eapply derives_trans, fupd.fupd_trans.
    apply fupd.fupd_mono, fupd.fupd_frame_l.
  - apply fupd.fupd_mono, sepcon_derives, fupd.fupd_intro; auto.
Qed.

Lemma proj_fupd_ret_assert_frame: forall F Q ek vl rho,
  fupd (F * proj_ret_assert (fupd_ret_assert Q) ek vl rho) = fupd (F * proj_ret_assert Q ek vl rho).
Proof.
  intros.
  destruct ek; simpl; auto;
    rewrite <- fupd_fupd_frame_l, fupd_fupd_andp_prop, fupd_fupd_frame_l; auto.
Qed.

Lemma rguard_fupd:
  forall {Espec: OracleKind} ge Delta F f (P: ret_assert) k,
    rguard Espec ge Delta f (frame_ret_assert P F) k = rguard Espec ge Delta f (frame_ret_assert (fupd_ret_assert P) F) k.
Proof.
  intros.
  unfold rguard.
  f_equal; extensionality ek.
  f_equal; extensionality vl.
  rewrite !proj_frame.
  destruct (eq_dec ek EK_return); subst; auto.
  rewrite _guard_fupd'; [|apply exit_cont_nonret; auto].
  setoid_rewrite _guard_fupd' at 2; [|apply exit_cont_nonret; auto].
  apply pred_ext; apply _guard_mono; intros; rewrite proj_fupd_ret_assert_frame; auto.
Qed.

Lemma _guard_allp_fun_id:
  forall {Espec: OracleKind} ge Delta' Delta f (F P: environ -> pred rmap) k,
    tycontext_sub Delta Delta' ->
    _guard Espec ge Delta' f (fun rho => F rho * P rho) k = _guard Espec ge Delta' f (fun rho => F rho * (allp_fun_id Delta rho && P rho)) k.
Proof.
  intros.
  unfold _guard.
  f_equal; extensionality tx.
  f_equal; extensionality vx.
  f_equal.
  f_equal.
  rewrite !andp_assoc.
  f_equal.
  rewrite corable_sepcon_andp1 by apply corable_allp_fun_id.
  rewrite (andp_comm (allp_fun_id _ _ )), andp_assoc.
  f_equal.
  apply pred_ext; [apply andp_right; auto | apply andp_left2; auto].
  intros w W. hnf.
  eapply funassert_allp_fun_id_sub; eauto.
Qed.

Lemma guard_allp_fun_id: forall {Espec: OracleKind} ge Delta' Delta f (F P: environ -> pred rmap) k,
  tycontext_sub Delta Delta' ->
  guard Espec ge Delta' f (fun rho => F rho * P rho) k = guard Espec ge Delta' f (fun rho => F rho * (allp_fun_id Delta rho && P rho)) k.
Proof.
  intros.
  apply _guard_allp_fun_id; auto.
Qed.

Lemma rguard_allp_fun_id: forall {Espec: OracleKind} ge Delta' Delta f (F: environ -> pred rmap) P k,
  tycontext_sub Delta Delta' ->
  rguard Espec ge Delta' f (frame_ret_assert P F) k = rguard Espec ge Delta' f (frame_ret_assert (conj_ret_assert P (allp_fun_id Delta)) F) k.
Proof.
  intros.
  unfold rguard.
  f_equal; extensionality ek.
  f_equal; extensionality vl.
  rewrite !proj_frame.
  rewrite proj_conj.
  apply _guard_allp_fun_id; auto.
Qed.

Lemma _guard_tc_environ:
  forall {Espec: OracleKind} ge Delta' Delta f (F P: environ -> pred rmap) k,
    tycontext_sub Delta Delta' ->
    _guard Espec ge Delta' f (fun rho => F rho * P rho) k =
    _guard Espec ge Delta' f (fun rho => F rho * (!! typecheck_environ Delta rho && P rho)) k.
Proof.
  intros.
  unfold _guard.
  f_equal; extensionality tx.
  f_equal; extensionality vx.
  f_equal.
  f_equal.
  f_equal.
  rewrite corable_sepcon_andp1 by apply corable_prop.
  rewrite <- andp_assoc.
  f_equal.
  apply pred_ext; [apply andp_right; auto | apply andp_left1; auto].
  intros ? ?; simpl in *.
  destruct H0 as [? _].
  eapply typecheck_environ_sub; eauto.
Qed.

Lemma guard_tc_environ: forall {Espec: OracleKind} ge Delta' Delta f (F P: environ -> pred rmap) k,
  tycontext_sub Delta Delta' ->
  guard Espec ge Delta' f (fun rho => F rho * P rho) k = guard Espec ge Delta' f (fun rho => F rho * (!! typecheck_environ Delta rho && P rho)) k.
Proof.
  intros.
  apply _guard_tc_environ; auto.
Qed.

Lemma rguard_tc_environ: forall {Espec: OracleKind} ge Delta' Delta f (F: environ -> pred rmap) P k,
  tycontext_sub Delta Delta' ->
  rguard Espec ge Delta' f (frame_ret_assert P F) k = rguard Espec ge Delta'  f (frame_ret_assert (conj_ret_assert P (fun rho => !! typecheck_environ Delta rho)) F) k.
Proof.
  intros.
  unfold rguard.
  f_equal; extensionality ek.
  f_equal; extensionality vl.
  rewrite !proj_frame.
  rewrite proj_conj.
  apply _guard_tc_environ; auto.
Qed.

Lemma semax_conseq {CS: compspecs} {Espec: OracleKind}:
 forall Delta P' (R': ret_assert) P c (R: ret_assert) ,
   (forall rho,  seplog.derives (!!(typecheck_environ Delta rho) && (allp_fun_id Delta rho && P rho))
                   (fupd (P' rho)) ) ->
   (forall rho,  seplog.derives (!!(typecheck_environ Delta rho) && (allp_fun_id Delta rho && RA_normal R' rho))
                   (fupd (RA_normal R rho))) ->
   (forall rho, seplog.derives (!! (typecheck_environ Delta rho) && (allp_fun_id Delta rho && RA_break R' rho))
                   (fupd (RA_break R rho))) ->
   (forall rho, seplog.derives (!! (typecheck_environ Delta rho) && (allp_fun_id Delta rho && RA_continue R' rho))
                   (fupd (RA_continue R rho))) ->
   (forall vl rho, seplog.derives (!! (typecheck_environ Delta rho) && (allp_fun_id Delta rho && RA_return R' vl rho))
                   (RA_return R vl rho)) ->
   semax Espec Delta P' c R' ->  semax Espec Delta P c R.
Proof.
  intros.
  assert (semax' Espec Delta P' c R' |-- semax' Espec Delta P c R);
    [clear H4 | exact (fun n => H5 n (H4 n))].
  rewrite semax_fold_unfold.
  apply allp_derives; intros gx.
  apply allp_derives; intros Delta'.
  apply allp_derives; intros CS'.
  apply prop_imp_derives; intros [? _].
  apply imp_derives; auto.
  apply allp_derives; intros k.
  apply allp_derives; intros F.
  apply allp_derives; intros f.
  apply imp_derives; [apply andp_derives; auto |].
  + erewrite (rguard_allp_fun_id _ _ _ _ _ R') by eauto.
    erewrite (rguard_tc_environ _ _ _ _ _ (conj_ret_assert R' _)) by eauto.
    rewrite (rguard_fupd _ _ _ _ R).
    apply rguard_mono.
    intros.
    rewrite proj_frame, proj_conj, proj_conj.
    destruct rk; simpl;
         [rename H0 into Hx; pose (ek:=RA_normal)
         | rename H1 into Hx; pose (ek:=RA_break)
         | rename H2 into Hx ; pose (ek:=RA_continue)
         | rewrite (sepcon_comm _ (F rho)); apply sepcon_derives, H3; auto]; clear H3.
all: rewrite <- sepcon_andp_prop1; rewrite sepcon_comm; apply sepcon_derives, derives_refl.
all:    specialize (Hx rho); inv Hx; simpl in *;
    apply derives_trans with (!! (vl = None) &&
       (!! typecheck_environ Delta rho &&
        (allp_fun_id Delta rho && ek R' rho))); subst ek;
     [  intros ? [? [? [? ?]]];  split3; auto; split; auto | ];
    apply prop_andp_left; intro Hvl;
    rewrite (prop_true_andp _ _ Hvl); auto.
  + erewrite (guard_allp_fun_id _ _ _ _ _ P) by eauto.
    erewrite (guard_tc_environ _ _ _ _ _ (fun rho => allp_fun_id Delta rho && P rho)) by eauto.
    rewrite (guard_fupd _ _ _ _ P').
    apply guard_mono.
    intros.
    apply sepcon_derives; auto.
    specialize (H rho); inv H; auto.
Qed.

(* Part 2: Deriving simpler and older version of consequence rules from semax_conseq. *)
Lemma semax'_post_fupd:
 forall {CS: compspecs} {Espec: OracleKind} (R': ret_assert) Delta (R: ret_assert) P c,
   (forall ek vl rho, ek <> EK_return -> !!(typecheck_environ Delta rho) &&
                proj_ret_assert R' ek vl rho
         |-- fupd (proj_ret_assert R ek vl rho)) ->
   (forall vl rho,  !!(typecheck_environ Delta rho) &&
                RA_return R' vl rho
         |-- RA_return R vl rho) ->
   semax' Espec Delta P c R' |-- semax' Espec Delta P c R.
Proof.
intros.
rewrite semax_fold_unfold.
apply allp_derives; intro psi.
apply allp_derives; intro Delta'.
apply allp_derives; intro CS'.
apply prop_imp_derives; intros [TS HGG].
apply imp_derives; auto.
apply allp_derives; intro k.
apply allp_derives; intro F.
apply allp_derives; intro f.
apply imp_derives; auto.
apply andp_derives; auto.
erewrite (rguard_tc_environ _ _ _ _ _ R') by eauto.
rewrite rguard_fupd.
apply rguard_mono; intros.
destruct (eq_dec rk EK_return); subst.
- destruct R, R'; simpl in *.
  rewrite andp_comm; apply sepcon_derives; auto.
- destruct R, R'; simpl in *.
  specialize (H rk vl rho); destruct rk; try contradiction; simpl in *;
    apply prop_andp_left; intros Hvl; rewrite (prop_true_andp _ _ Hvl) in H;
    rewrite prop_true_andp by auto; rewrite andp_comm; apply sepcon_derives; auto;
    eapply derives_trans, fupd.fupd_mono, andp_left2; try apply H; auto.
Qed.

Lemma semax'_post:
 forall {CS: compspecs} {Espec: OracleKind} (R': ret_assert) Delta (R: ret_assert) P c,
   (forall ek vl rho,  !!(typecheck_environ Delta rho) &&
                proj_ret_assert R' ek vl rho
         |-- proj_ret_assert R ek vl rho) ->
   semax' Espec Delta P c R' |-- semax' Espec Delta P c R.
Proof.
intros.
apply semax'_post_fupd.
intros; eapply derives_trans, fupd.fupd_intro; auto.
intros; apply (H EK_return).
Qed.

Lemma semax'_pre_fupd:
 forall {CS: compspecs} {Espec: OracleKind} P' Delta R P c,
  (forall rho, typecheck_environ Delta rho ->   P rho |-- fupd (P' rho))
   ->   semax' Espec Delta P' c R |-- semax' Espec Delta P c R.
Proof.
intros.
repeat rewrite semax_fold_unfold.
apply allp_derives; intro psi.
apply allp_derives; intro Delta'.
apply allp_derives; intro CS'.
apply prop_imp_derives; intros [TS HGG].
apply imp_derives; auto.
apply allp_derives; intro k.
apply allp_derives; intro F.
apply allp_derives; intro f.
apply imp_derives; auto.
erewrite (guard_tc_environ _ _ _ _ _ (fun rho => P rho)) by eauto.
rewrite (guard_fupd _ _ _ _ P').
apply guard_mono.
intros.
apply sepcon_derives; auto.
apply prop_andp_left; auto.
Qed.

Lemma semax'_pre:
 forall {CS: compspecs} {Espec: OracleKind} P' Delta R P c,
  (forall rho, typecheck_environ Delta rho ->   P rho |-- P' rho)
   ->   semax' Espec Delta P' c R |-- semax' Espec Delta P c R.
Proof.
intros; apply semax'_pre_fupd.
intros; eapply derives_trans, fupd.fupd_intro; auto.
Qed.

Lemma semax'_pre_post_fupd:
 forall
      {CS: compspecs} {Espec: OracleKind} P' (R': ret_assert) Delta (R: ret_assert) P c,
   (forall rho, typecheck_environ Delta rho ->   P rho |-- fupd (P' rho)) ->
   (forall ek vl rho, ek <> EK_return -> !!(typecheck_environ Delta rho)
                       &&  proj_ret_assert R ek vl rho
                    |-- fupd (proj_ret_assert R' ek vl rho)) ->
   (forall vl rho, !!(typecheck_environ Delta rho)
                       &&  RA_return R vl rho
                    |-- RA_return R' vl rho) ->
   semax' Espec Delta P' c R |-- semax' Espec Delta P c R'.
Proof.
intros.
eapply derives_trans.
apply semax'_pre_fupd; eauto.
apply semax'_post_fupd; auto.
Qed.

Lemma semax'_pre_post:
 forall
      {CS: compspecs} {Espec: OracleKind} P' (R': ret_assert) Delta (R: ret_assert) P c,
   (forall rho, typecheck_environ Delta rho ->   P rho |-- P' rho) ->
   (forall ek vl rho, !!(typecheck_environ Delta rho)
                       &&  proj_ret_assert R ek vl rho
                    |-- proj_ret_assert R' ek vl rho) ->
   semax' Espec Delta P' c R |-- semax' Espec Delta P c R'.
Proof.
intros.
eapply derives_trans.
apply semax'_pre; eauto.
apply semax'_post; auto.
Qed.

Lemma semax_post'_fupd {CS: compspecs} {Espec: OracleKind}:
 forall (R': ret_assert) Delta (R: ret_assert) P c,
   (forall ek vl rho, ek <> EK_return -> !!(typecheck_environ Delta rho)
                      &&  proj_ret_assert R' ek vl rho
                        |-- fupd (proj_ret_assert R ek vl rho)) ->
   (forall vl rho,  !!(typecheck_environ Delta rho)
                      &&  RA_return R' vl rho
                        |-- RA_return R vl rho) ->
   semax Espec Delta P c R' ->  semax Espec Delta P c R.
Proof.
unfold semax.
intros.
specialize (H1 n). revert n H1.
apply semax'_post_fupd; auto.
Qed.

Lemma semax_post_fupd {CS: compspecs} {Espec: OracleKind}:
 forall (R': ret_assert) Delta (R: ret_assert) P c,
   (forall rho,  !!(typecheck_environ Delta rho)
                      &&  RA_normal R' rho |-- fupd (RA_normal R rho)) ->
   (forall rho, !! (typecheck_environ Delta rho)
                      && RA_break R' rho |-- fupd (RA_break R rho)) ->
   (forall rho, !! (typecheck_environ Delta rho)
                      && RA_continue R' rho |-- fupd (RA_continue R rho)) ->
   (forall vl rho, !! (typecheck_environ Delta rho)
                      && RA_return R' vl rho |-- RA_return R vl rho) ->
   semax Espec Delta P c R' ->  semax Espec Delta P c R.
Proof.
unfold semax.
intros.
specialize (H3 n). revert n H3.
apply semax'_post_fupd; auto.
intros; destruct ek; try contradiction; simpl;
repeat (apply normalize.derives_extract_prop; intro); rewrite ?prop_true_andp by auto;
specialize (H rho); specialize (H0 rho); specialize (H1 rho); specialize (H2 vl rho);
rewrite ?prop_true_andp in H, H0, H1, H2 by auto; auto.
Qed.

Lemma semax_post' {CS: compspecs} {Espec: OracleKind}:
 forall (R': ret_assert) Delta (R: ret_assert) P c,
   (forall ek vl rho,  !!(typecheck_environ Delta rho)
                      &&  proj_ret_assert R' ek vl rho
                        |-- proj_ret_assert R ek vl rho) ->
   semax Espec Delta P c R' ->  semax Espec Delta P c R.
Proof.
unfold semax.
intros.
specialize (H0 n). revert n H0.
apply semax'_post.
auto.
Qed.

Lemma semax_post {CS: compspecs} {Espec: OracleKind}:
 forall (R': ret_assert) Delta (R: ret_assert) P c,
   (forall rho,  !!(typecheck_environ Delta rho)
                      &&  RA_normal R' rho |-- RA_normal R rho) ->
   (forall rho, !! (typecheck_environ Delta rho)
                      && RA_break R' rho |-- RA_break R rho) ->
   (forall rho, !! (typecheck_environ Delta rho)
                      && RA_continue R' rho |-- RA_continue R rho) ->
   (forall vl rho, !! (typecheck_environ Delta rho)
                      && RA_return R' vl rho |-- RA_return R vl rho) ->
   semax Espec Delta P c R' ->  semax Espec Delta P c R.
Proof.
unfold semax.
intros.
specialize (H3 n). revert n H3.
apply semax'_post.
intros; destruct ek; simpl;
repeat (apply normalize.derives_extract_prop; intro); rewrite ?prop_true_andp by auto;
specialize (H rho); specialize (H0 rho); specialize (H1 rho); specialize (H2 vl rho);
rewrite prop_true_andp in H, H0, H1, H2 by auto; auto.
Qed.

Lemma semax_pre_fupd {CS: compspecs} {Espec: OracleKind} :
 forall P' Delta P c R,
   (forall rho,  !!(typecheck_environ Delta rho) &&  P rho |-- fupd (P' rho) )%pred ->
     semax Espec Delta P' c R  -> semax Espec Delta P c R.
Proof.
unfold semax.
intros.
specialize (H0 n).
revert n H0.
apply semax'_pre_fupd.
intros ????. apply (H rho a); auto. split; auto.
Qed.

Lemma semax_pre {CS: compspecs} {Espec: OracleKind} :
 forall P' Delta P c R,
   (forall rho,  !!(typecheck_environ Delta rho) &&  P rho |-- P' rho )%pred ->
     semax Espec Delta P' c R  -> semax Espec Delta P c R.
Proof.
unfold semax.
intros.
specialize (H0 n).
revert n H0.
apply semax'_pre.
intros ????. apply (H rho a). split; auto.
Qed.

Lemma semax_pre_post_fupd {CS: compspecs} {Espec: OracleKind}:
 forall P' (R': ret_assert) Delta P c (R: ret_assert) ,
   (forall rho,  !!(typecheck_environ Delta rho) &&  P rho |-- fupd (P' rho) )%pred ->
   (forall rho,  !!(typecheck_environ Delta rho)
                      &&  RA_normal R' rho |-- fupd (RA_normal R rho)) ->
   (forall rho, !! (typecheck_environ Delta rho)
                      && RA_break R' rho |-- fupd (RA_break R rho)) ->
   (forall rho, !! (typecheck_environ Delta rho)
                      && RA_continue R' rho |-- fupd (RA_continue R rho)) ->
   (forall vl rho, !! (typecheck_environ Delta rho)
                      && RA_return R' vl rho |-- RA_return R vl rho) ->
   semax Espec Delta P' c R' ->  semax Espec Delta P c R.
Proof.
intros.
eapply semax_pre_fupd; eauto.
eapply semax_post_fupd; eauto.
Qed.

Lemma semax_pre_post {CS: compspecs} {Espec: OracleKind}:
 forall P' (R': ret_assert) Delta P c (R: ret_assert) ,
   (forall rho,  !!(typecheck_environ Delta rho) &&  P rho |-- P' rho )%pred ->
   (forall rho,  !!(typecheck_environ Delta rho)
                      &&  RA_normal R' rho |-- RA_normal R rho) ->
   (forall rho, !! (typecheck_environ Delta rho)
                      && RA_break R' rho |-- RA_break R rho) ->
   (forall rho, !! (typecheck_environ Delta rho)
                      && RA_continue R' rho |-- RA_continue R rho) ->
   (forall vl rho, !! (typecheck_environ Delta rho)
                      && RA_return R' vl rho |-- RA_return R vl rho) ->
   semax Espec Delta P' c R' ->  semax Espec Delta P c R.
Proof.
intros.
eapply semax_pre; eauto.
eapply semax_post; eauto.
Qed.

Lemma semax_fupd_elim {CS: compspecs} {Espec: OracleKind}:
 forall Delta P c R,
  semax Espec Delta P c R -> semax Espec Delta (fun rho => fupd (P rho)) c R.
Proof.
intros ????; apply semax_pre_fupd.
intro; apply prop_andp_left; auto.
Qed.

Lemma semax_skip {CS: compspecs} {Espec: OracleKind}:
   forall Delta P, semax Espec Delta P Sskip (normal_ret_assert P).
Proof.
intros.
apply derives_skip.
intros.
simpl.
rewrite prop_true_andp by auto.
auto.
Qed.

(*Taken from floyd.SeparationLogicFacts.v*)
Lemma semax_extract_prop:
  forall {CS: compspecs} {Espec: OracleKind},
  forall Delta (PP: Prop) (P:assert) c (Q:ret_assert),
           (PP -> @semax CS Espec Delta P c Q) ->
           @semax CS Espec Delta (fun rho => !!PP && P rho) c Q.
Proof.
  intros.
  eapply semax_pre with (fun rho => EX H: PP, P rho).
  + intros. apply andp_left2.
    apply normalize.derives_extract_prop; intros.
    apply (exp_right H0), derives_refl.
  + apply extract_exists_pre, H.
Qed.

Lemma semax_adapt_frame {cs Espec} Delta c (P P': assert) (Q Q' : ret_assert)
   (H: forall rho,  derives (!!(typecheck_environ Delta rho) && (allp_fun_id Delta rho && P rho))
                   (EX F: assert, (!!(closed_wrt_modvars c F) && fupd (P' rho * F rho) &&
                         !!(forall rho, (local (tc_environ Delta) rho) && ((allp_fun_id Delta rho)) && RA_normal (frame_ret_assert Q' F) rho |-- fupd (RA_normal Q rho)) &&
                         !!(forall rho, (local (tc_environ Delta) rho) && ((allp_fun_id Delta rho)) && RA_break (frame_ret_assert Q' F) rho |-- fupd (RA_break Q rho)) &&
                         !!(forall rho, (local (tc_environ Delta) rho) && ((allp_fun_id Delta rho)) && RA_continue (frame_ret_assert Q' F) rho |-- fupd (RA_continue Q rho)) &&
                         !!(forall vl rho, (local (tc_environ Delta) rho) && ((allp_fun_id Delta rho)) && RA_return (frame_ret_assert Q' F) vl rho |-- RA_return Q vl rho))))
   (SEM: @semax cs Espec Delta P' c Q'):
   @semax cs Espec Delta P c Q.
Proof. intros.
apply (semax_conseq Delta (fun rho => EX F: assert, !!(closed_wrt_modvars c F) && (fupd (sepcon (P' rho) (F rho)) &&
                         (!!(forall rho, (local (tc_environ Delta) rho) && ((allp_fun_id Delta rho)) && RA_normal (frame_ret_assert Q' F) rho |-- fupd (RA_normal Q rho)) &&
                         (!!(forall rho, (local (tc_environ Delta) rho) && ((allp_fun_id Delta rho)) && RA_break (frame_ret_assert Q' F) rho |-- fupd (RA_break Q rho)) &&
                         (!!(forall rho, (local (tc_environ Delta) rho) && ((allp_fun_id Delta rho)) && RA_continue (frame_ret_assert Q' F) rho |-- fupd (RA_continue Q rho)) &&
                         (!!(forall vl rho, (local (tc_environ Delta) rho) && ((allp_fun_id Delta rho)) && RA_return (frame_ret_assert Q' F) vl rho |-- RA_return Q vl rho)))))))
   Q).
+ intros. eapply seplog.derives_trans. constructor. apply H. clear H.
  eapply seplog.derives_trans. 2: { constructor. apply fupd.fupd_intro. }
  constructor. apply exp_derives; intros F.
  rewrite <- ! andp_assoc; trivial.
+ clear H. intros. constructor. eapply derives_trans, fupd.fupd_intro.
  do 2 apply andp_left2; trivial.
+ clear H. intros. constructor. eapply derives_trans, fupd.fupd_intro.
  do 2 apply andp_left2; trivial.
+ clear H. intros. constructor. eapply derives_trans, fupd.fupd_intro.
  do 2 apply andp_left2; trivial.
+ clear H. intros. constructor.
  do 2 apply andp_left2; trivial.
+ apply extract_exists_pre. intros F. clear H.
  apply semax_extract_prop. intros.
  eapply semax_pre_fupd. 2:{ do 4 (apply semax_extract_prop; intros).
    eapply semax_conseq. 6:{ apply semax_frame. exact H. apply SEM. }
    2: {
    intros; constructor.
    revert rho. exact H0. }
    2: {
    intros; constructor.
    revert rho. exact H1. }
    2: {
    intros; constructor.
    revert rho. exact H2. }
    2: {
    intros; constructor.
    revert rho. revert vl. exact H3. }

   intros; constructor. eapply derives_trans; [ | apply fupd.fupd_intro].
   apply andp_left2. apply andp_left2. apply derives_refl. }
  intros. unfold local, liftx, lift1, tc_environ; simpl. apply andp_left2.
  rewrite (andp_comm (fupd (P' rho * F rho))). eapply derives_trans, fupd.fupd_andp_prop.
  rewrite andp_assoc; apply andp_derives; [apply prop_derives; intros; rewrite <- andp_assoc; auto|].
  eapply derives_trans, fupd.fupd_andp_prop.
  rewrite andp_assoc; apply andp_derives; [apply prop_derives; intros; rewrite <- andp_assoc; auto|].
  eapply derives_trans, fupd.fupd_andp_prop.
  rewrite andp_assoc; apply andp_derives; [apply prop_derives; intros; rewrite <- andp_assoc; auto|].
  eapply derives_trans, fupd.fupd_andp_prop.
  apply andp_derives; [apply prop_derives; intros; rewrite <- andp_assoc; auto|].
  auto.
Qed.

Lemma semax_adapt_frame' {cs Espec} Delta c (P P': assert) (Q Q' : ret_assert)
   (H: forall rho,  !!(typecheck_environ Delta rho) && (allp_fun_id Delta rho && P rho)
                   |-- EX F: assert, (!!(closed_wrt_modvars c F) && fupd (P' rho * F rho) &&
                        !!(forall rho, RA_normal (frame_ret_assert Q' F) rho |-- fupd (RA_normal Q rho)) &&
                        !!(forall rho, RA_break (frame_ret_assert Q' F) rho |-- fupd (RA_break Q rho)) &&
                        !!(forall rho, RA_continue (frame_ret_assert Q' F) rho |-- fupd (RA_continue Q rho)) &&
                        !!(forall vl rho, RA_return (frame_ret_assert Q' F) vl rho |-- RA_return Q vl rho)))
   (SEM: @semax cs Espec Delta P' c Q'):
   @semax cs Espec Delta P c Q.
Proof.
  intros. eapply semax_adapt_frame. 2: apply SEM.
  intros. eapply derives_trans. apply H.
  clear. apply exp_derives. intros FR.
  rewrite ! andp_assoc.
  apply andp_derives; trivial.
  apply andp_derives; trivial.
  apply andp_derives.
  { apply prop_derives; intros. eapply derives_trans. 2: apply H. apply andp_left2; trivial. }
  apply andp_derives.
  { apply prop_derives; intros. eapply derives_trans. 2: apply H. apply andp_left2; trivial. }
  apply andp_derives.
  { apply prop_derives; intros. eapply derives_trans. 2: apply H. apply andp_left2; trivial. }
  { apply prop_derives; intros. eapply derives_trans. 2: apply H. apply andp_left2; trivial. }
Qed.

Lemma semax_adapt {cs Espec} Delta c (P P': assert) (Q Q' : ret_assert)
   (H: forall rho,  !!(typecheck_environ Delta rho) && (allp_fun_id Delta rho && P rho)
                   |-- (fupd (P' rho) &&
                        !!(forall rho, RA_normal Q' rho |-- fupd (RA_normal Q rho)) &&
                        !!(forall rho, RA_break Q' rho |-- fupd (RA_break Q rho)) &&
                        !!(forall rho, RA_continue Q' rho |-- fupd (RA_continue Q rho)) &&
                        !!(forall vl rho, RA_return Q' vl rho |-- RA_return Q vl rho)))
   (SEM: @semax cs Espec Delta P' c Q'):
   @semax cs Espec Delta P c Q.
Proof.
  intros. eapply semax_adapt_frame'; eauto. intros. exists (fun rho => emp).
  apply H in H0; clear H.
  destruct H0 as [[[[HP' NORM] BREAK] CONT] RET]. simpl in NORM, BREAK, CONT, RET.
  rewrite sepcon_emp. repeat split; auto; simpl; intros.
  + eapply derives_trans; [ | apply NORM]; clear.
    destruct Q'; simpl; rewrite sepcon_emp; trivial.
  + eapply derives_trans; [ | apply BREAK]; clear.
    destruct Q'; simpl; rewrite sepcon_emp; trivial.
  + eapply derives_trans; [ | apply CONT]; clear.
    destruct Q'; simpl; rewrite sepcon_emp; trivial.
  + eapply derives_trans; [ | apply RET]; clear.
    destruct Q'; simpl; rewrite sepcon_emp; trivial.
Qed.

author: PrincetonUniversity

repo: VST


text:
From Undecidability.L Require Import Tactics.LTactics.
Require Import Numbers.BinNums.
From Undecidability.L.Datatypes Require Import LNat LBool.
From Complexity.L Require Import LBinNums LComparison.

Import Nat.
#[export]
Instance termT_Pos_compare_cont : computableTime' Pos.compare_cont (fun _ _ => (5,fun x _ => (1,fun y _ => (min (Pos.size_nat x) (Pos.size_nat y)*17,tt)))).
Proof.
  unfold Pos.compare_cont.
  extract. solverec.
Qed.

#[export]
Instance term_Pos_compare : computableTime' Pos.compare (fun x _ => (7,fun y _ => (min (Pos.size_nat x) (Pos.size_nat y)*17,tt))).
Proof.
  change Pos.compare with (fun x => Pos.compare x). unfold Pos.compare. set (WorkAround:=Pos.compare_cont).
  extract. solverec.
Qed.

#[export]
Instance termT_N_compare : computableTime' N.compare (fun x _ => (1,fun y _ => (min (N.size_nat x) (N.size_nat y)*17+ 16,tt))).
Proof.
  unfold N.compare. set (WorkAround:=Pos.compare).
  extract. solverec.
Qed.

Import N.
#[export]
Instance termT_N_leb : computableTime' N.leb (fun x _ => (1,fun y _ => (Nat.min (N.size_nat x) (N.size_nat y)*17+ 22,tt))).
Proof.
  extract. solverec.
Qed.

#[export]
Instance termT_N_ltb : computableTime' N.ltb  (fun x _ => (1,fun y _ => (Nat.min (N.size_nat x) (N.size_nat y)*17+ 22,tt))).
Proof.
  extract. solverec.
Qed.

#[export]
Instance termT_N_eqb : computableTime' N.eqb  (fun x _ => (1,fun y _ => (Nat.min (N.size_nat x) (N.size_nat y)*17+ 22,tt))).
Proof.
  eapply computableTimeExt with (x:=fun x y : N => match (x ?= y)%N with
                       | Eq => true
                       | _ => false
                                                end).
  -repeat intro. hnf. now rewrite N.eqb_compare.
  -extract. solverec.
Qed.

author: uds-psl

repo: coq-library-complexity


text:
Require Import Gc.Language Gc.Gc Gc.Util.
Require Import List ListSet CpdtTactics Equality Wf Nat Wf_nat.

Lemma subset_property: forall st v p p0 roots,
  (exists address v0 p', roots_maps (roots) v0 p' /\ addresses (heap st) p' address p0) ->
  (exists address v0 p', roots_maps ((v, p) :: roots) v0 p' /\ addresses (heap st) p' address p0)
.
Proof.
  intros.
  destruct H as [a [v0 [p' H]]].
  exists a.
  exists v0.
  exists p'.
  unfold roots_maps.
  crush.
Qed.

Lemma mark_liveness_1 :
  forall r h p vs,
    set_In p (mark r h) ->
    heap_maps_struct h p vs ->
    exists address p' v,
      roots_maps r v p'
      /\
      addresses h p' address p
.
Proof.
  Hint Unfold heap_maps_struct heap_get_struct roots_maps.
  Hint Resolve subset_property.
  Hint Constructors addresses.
  induction r. crush.
  intros.
  specialize (IHr h p vs).

  unfold mark in H ; fold mark in H.
  destruct a.
  destruct (ptr_eq_dec p p0).
  * subst.
    clear IHr.
    exists TermStr.
    exists p0. exists v.
    split. crush.
    eauto.
  * specialize (mark_ptrs_correct _ h p  _ _ H).
    intros.
    intuition.
    destruct H1. destruct H1. destruct H1.
    exists x0. exists x.
    unfold roots_maps.
    specialize (nodup_In_fwd _ _ ptr_eq_dec H1). clear H1. intros.
    specialize (set_inter_elim1 _ _ _ _ H1). clear H1. intros.
    apply in_split_exists_r in H1.
    - destruct H1. exists x1. crush.
    - apply ptr_eq_dec.
Qed.

Lemma mark_sweep_liveness_1 :
  forall st p vs h,
    sweep (heap st) (mark (roots st) (heap st)) = h ->
    heap_maps_struct h p vs ->
    exists address p' v,
      roots_maps (roots st) v p'
      /\
      addresses (heap st) p' address p
.
Proof.
  intros.
  apply (sweep_actually_sweeps (heap st) h (mark (roots st) (heap st)) p vs) in H.
  * destruct H.
    eapply (mark_liveness_1).
    + apply H.
    + apply H1.
  * intuition.
Qed.

Theorem mark_sweep_liveness_2 :
  forall st p vs h,
    (mark_sweep (roots st) (heap st)) = h ->
    heap_maps_struct h p vs ->
    exists address v p',
      roots_maps (roots st) v p'
      /\
      addresses h p' address p
.
Proof.
  intros.
  pose H as temp.
  apply (mark_sweep_liveness_1 st p vs h) in temp.
  * destruct temp as [a [v  [p' [H1 H2]]]].
    eapply pointer_equivalence in H2; eauto.
    exists a, p', v.
    crush.
  * auto.
Qed.

Theorem gc_liveness :
  forall st st' p vs h,
    gc st = st' ->
    (heap st') = h ->
    heap_maps_struct h p vs ->
    exists address v p',
      roots_maps (roots st') v p'
      /\
      addresses h p' address p
.
Proof.
  Hint Unfold gc compact.
  Hint Resolve mark_sweep_liveness_2.
  intros.
  subst.
  unfold gc in *.
  unfold compact in *.
  unfold roots in *.
  unfold heap in *.
  eapply mark_sweep_liveness_2; eauto.
Qed.

author: alexrenda

repo: verified-gc

save_path: github-repos/coq/alexrenda-verified-gc