text:
(**
This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
#
#
Copyright (C) 2011-2015 Catherine Lelay
#
#
Copyright (C) 2011-2015 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
---------------------------------------------------------------
This version modified to work without SSReflect,
or any other dependencies, as part of the QWIRE project
by Robert Rand and Jennifer Paykin (June 2017).
*)

Require Export Prelim.
Require Export RealAux.

(*********************)
(** Complex Numbers **)
(*********************)

(** This file defines complex numbers [C] as [R * R]. Operations are
given, and [C] is proved to be a field, a normed module, and a
complete space. *)

(** * The set of complex numbers *)

Definition C := (R * R)%type.

Declare Scope C_scope.
Delimit Scope C_scope with C.

Open Scope nat_scope.
Open Scope R_scope.
Open Scope C_scope.
Bind Scope nat_scope with nat.
Bind Scope R_scope with R.
Bind Scope C_scope with C.

Definition RtoC (x : R) : C := (x,0).
Coercion RtoC : R >-> C.

Lemma RtoC_inj : forall (x y : R),
  RtoC x = RtoC y -> x = y.
Proof.
  intros x y H.
  now apply (f_equal (@fst R R)) in H.
Qed.

Lemma Ceq_dec (z1 z2 : C) : { z1 = z2 } + { z1 <> z2 }.
Proof.
  destruct z1 as [x1 y1].
  destruct z2 as [x2 y2].
  destruct (Req_EM_T x1 x2) as [Eqx | Neqx]; [| right; congruence].
  destruct (Req_EM_T y1 y2) as [Eqy | Neqy]; [subst; auto | right; congruence].
Qed.

(** ** Constants and usual functions *)

(** 0 and 1 for complex are defined as [RtoC 0] and [RtoC 1] *)
Definition Ci : C := (0,1).

(** *** Arithmetic operations *)

Definition Cplus (x y : C) : C := (fst x + fst y, snd x + snd y).
Definition Copp (x : C) : C := (-fst x, -snd x).
Definition Cminus (x y : C) : C := Cplus x (Copp y).
Definition Cmult (x y : C) : C := (fst x * fst y - snd x * snd y, fst x * snd y + snd x * fst y).
Definition Cinv (x : C) : C := (fst x / (fst x ^ 2 + snd x ^ 2), - snd x / (fst x ^ 2 + snd x ^ 2)).
Definition Cdiv (x y : C) : C := Cmult x (Cinv y).

Infix "+" := Cplus : C_scope.
Notation "- x" := (Copp x) : C_scope.
Infix "-" := Cminus : C_scope.
Infix "*" := Cmult : C_scope.
Notation "/ x" := (Cinv x) : C_scope.
Infix "/" := Cdiv : C_scope.

(* Added exponentiation *)
Fixpoint Cpow (c : C) (n : nat) : C :=
  match n with
  | 0%nat => 1
  | S n' => c * Cpow c n'
  end.

Infix "^" := Cpow : C_scope.

(** *** Other usual functions *)

Definition Re (z : C) : R := fst z.

Definition Im (z : C) : R := snd z.

Definition Cmod (x : C) : R := sqrt (fst x ^ 2 + snd x ^ 2).

Definition Cconj (x : C) : C := (fst x, (- snd x)%R).

Notation "a ^*" := (Cconj a) (at level 10) : C_scope.

Lemma Cmod_0 : Cmod 0 = R0.
Proof.
unfold Cmod.
simpl.
rewrite Rmult_0_l, Rplus_0_l.
apply sqrt_0.
Qed.
Lemma Cmod_1 : Cmod 1 = R1.
Proof.
unfold Cmod.
simpl.
rewrite Rmult_0_l, Rplus_0_r, 2!Rmult_1_l.
apply sqrt_1.
Qed.

Lemma Cmod_opp : forall x, Cmod (-x) = Cmod x.
Proof.
unfold Cmod.
simpl.
intros x.
apply f_equal.
ring.
Qed.

Lemma Cmod_triangle : forall x y, Cmod (x + y) <= Cmod x + Cmod y.
Proof.
  intros x y ; unfold Cmod.
  apply Rsqr_incr_0_var.
  apply Rminus_le_0.
  unfold Rsqr ; simpl ; ring_simplify.
  unfold pow.
  rewrite ?Rmult_1_r.
  rewrite ?sqrt_sqrt ; ring_simplify.
  replace (-2 * fst x * fst y - 2 * snd x * snd y)%R with (- (2 * (fst x * fst y + snd x * snd y)))%R by ring.
  rewrite Rmult_assoc, <- sqrt_mult.
  rewrite Rplus_comm.
  apply -> Rminus_le_0.
  apply Rmult_le_compat_l.
  apply Rlt_le, Rlt_0_2.
  apply Rsqr_incr_0_var.
  apply Rminus_le_0.
  unfold Rsqr; rewrite ?sqrt_sqrt ; ring_simplify.
  replace (fst x ^ 2 * snd y ^ 2 - 2 * fst x * snd x * fst y * snd y +
    snd x ^ 2 * fst y ^ 2)%R with ( (fst x * snd y - snd x * fst y)^2)%R
    by ring.
  apply pow2_ge_0.
  repeat apply Rplus_le_le_0_compat ; apply Rmult_le_pos ; apply pow2_ge_0.
  apply sqrt_pos.
  apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
  apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
  replace (fst x ^ 2 + 2 * fst x * fst y + fst y ^ 2 + snd x ^ 2 + 2 * snd x * snd y + snd y ^ 2)%R
    with ((fst x + fst y)^2 + (snd x + snd y)^2)%R by ring.
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
  apply Rplus_le_le_0_compat ; apply sqrt_pos.
Qed.

Lemma Cmod_mult : forall x y, Cmod (x * y) = (Cmod x * Cmod y)%R.
Proof.
  intros x y.
  unfold Cmod.
  rewrite <- sqrt_mult.
  apply f_equal ; simpl ; ring.
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
  apply Rplus_le_le_0_compat ; apply pow2_ge_0.
Qed.

Lemma Cmod_pow : forall x n, Cmod (x ^ n) = ((Cmod x) ^ n)%R.
Proof.
  intros x n.
  induction n; simpl.
  apply Cmod_1.
  rewrite Cmod_mult, IHn.
  reflexivity.
Qed.

Lemma Rmax_Cmod : forall x,
  Rmax (Rabs (fst x)) (Rabs (snd x)) <= Cmod x.
Proof.
  intros [x y]; simpl.
  rewrite <- !sqrt_Rsqr_abs.
  apply Rmax_case ; apply sqrt_le_1_alt, Rminus_le_0 ;
  unfold Rsqr; simpl ; ring_simplify ; try apply pow2_ge_0; auto.
Qed.
Lemma Cmod_2Rmax : forall x,
  Cmod x <= sqrt 2 * Rmax (Rabs (fst x)) (Rabs (snd x)).
Proof.
  intros [x y]; apply Rmax_case_strong; intros H0;
  rewrite <- !sqrt_Rsqr_abs ;
  rewrite <- ?sqrt_mult ;
  try (apply Rle_0_sqr; auto);
  try (apply Rlt_le, Rlt_0_2; auto) ;
  apply sqrt_le_1_alt ; simpl ; [ rewrite Rplus_comm | ] ;
  unfold Rsqr ; apply Rle_minus_r ; ring_simplify ;
  apply Rsqr_le_abs_1 in H0 ; unfold pow; rewrite !Rmult_1_r; auto.
Qed.

(** ** C is a field *)

Lemma RtoC_plus (x y : R) : RtoC (x + y) = RtoC x + RtoC y.
Proof.
  unfold RtoC, Cplus ; simpl.
  rewrite Rplus_0_r; auto.
Qed.

Lemma RtoC_opp (x : R) : RtoC (- x) = - RtoC x.
Proof.
  unfold RtoC, Copp ; simpl.
  rewrite Ropp_0; auto.
Qed.

Lemma RtoC_minus (x y : R) : RtoC (x - y) = RtoC x - RtoC y.
Proof. unfold Cminus; rewrite <- RtoC_opp, <- RtoC_plus; auto. Qed.

Lemma RtoC_mult (x y : R) : RtoC (x * y) = RtoC x * RtoC y.
Proof.
  unfold RtoC, Cmult ; simpl.
  apply injective_projections ; simpl ; ring.
Qed.

Lemma RtoC_inv (x : R) : (x <> 0)%R -> RtoC (/ x) = / RtoC x.
Proof. intros Hx. apply injective_projections ; simpl ; field ; auto. Qed.

Lemma RtoC_div (x y : R) : (y <> 0)%R -> RtoC (x / y) = RtoC x / RtoC y.
Proof. intros Hy. apply injective_projections ; simpl ; field ; auto. Qed.

Lemma Cplus_comm (x y : C) : x + y = y + x.
Proof. apply injective_projections ; simpl ; apply Rplus_comm. Qed.

Lemma Cplus_assoc (x y z : C) : x + (y + z) = (x + y) + z.
Proof. apply injective_projections ; simpl ; apply sym_eq, Rplus_assoc. Qed.

Lemma Cplus_0_r (x : C) : x + 0 = x.
Proof. apply injective_projections ; simpl ; apply Rplus_0_r. Qed.

Lemma Cplus_0_l (x : C) : 0 + x = x.
Proof. apply injective_projections ; simpl ; apply Rplus_0_l. Qed.

Lemma Cplus_opp_r (x : C) : x + -x = 0.
Proof. apply injective_projections ; simpl ; apply Rplus_opp_r. Qed.

Lemma Copp_plus_distr (z1 z2 : C) : - (z1 + z2) = (- z1 + - z2).
Proof. apply injective_projections ; apply Ropp_plus_distr; auto. Qed.

Lemma Copp_minus_distr (z1 z2 : C) : - (z1 - z2) = z2 - z1.
Proof. apply injective_projections ; apply Ropp_minus_distr; auto. Qed.

Lemma Cmult_comm (x y : C) : x * y = y * x.
Proof. apply injective_projections ; simpl ; ring. Qed.

Lemma Cmult_assoc (x y z : C) : x * (y * z) = (x * y) * z.
Proof. apply injective_projections ; simpl ; ring. Qed.

Lemma Cmult_0_r (x : C) : x * 0 = 0.
Proof. apply injective_projections ; simpl ; ring. Qed.

Lemma Cmult_0_l (x : C) : 0 * x = 0.
Proof. apply injective_projections ; simpl ; ring. Qed.

Lemma Cmult_1_r (x : C) : x * 1 = x.
Proof. apply injective_projections ; simpl ; ring. Qed.

Lemma Cmult_1_l (x : C) : 1 * x = x.
Proof. apply injective_projections ; simpl ; ring. Qed.

Lemma Cinv_r (r : C) : r <> 0 -> r * /r = 1.
Proof.
  intros H.
  apply injective_projections ; simpl ; field.
  contradict H.
  apply Rplus_sqr_eq_0 in H.
  apply injective_projections ; simpl ; apply H.
  contradict H.
  apply Rplus_sqr_eq_0 in H.
  apply injective_projections ; simpl ; apply H.
Qed.

Lemma Cinv_l (r : C) : r <> 0 -> /r * r = 1.
Proof.
intros Zr.
rewrite Cmult_comm.
now apply Cinv_r.
Qed.

Lemma Cmult_plus_distr_l (x y z : C) : x * (y + z) = x * y + x * z.
Proof.
  apply injective_projections ; simpl ; ring.
Qed.

Lemma Cmult_plus_distr_r (x y z : C) : (x + y) * z = x * z + y * z.
Proof.
  apply injective_projections ; simpl ; ring.
Qed.

(* I'll be leaving out mixins and Canonical Structures :
Definition C_AbelianGroup_mixin :=
  AbelianGroup.Mixin _ _ _ _ Cplus_comm Cplus_assoc Cplus_0_r Cplus_opp_r.
Canonical C_AbelianGroup :=
  AbelianGroup.Pack C C_AbelianGroup_mixin C.
*)

Lemma Copp_0 : Copp 0 = 0.
Proof. apply injective_projections; simpl ; ring. Qed.

Lemma Cmod_m1 : Cmod (Copp 1) = 1.
Proof. rewrite Cmod_opp. apply Cmod_1. Qed.

Lemma Cmod_eq_0 : forall x, Cmod x = 0 -> x = 0.
Proof.
  intros x H.
  unfold Cmod, pow in H.
  rewrite 2!Rmult_1_r, <- sqrt_0 in H.
  apply sqrt_inj in H.
  apply Rplus_sqr_eq_0 in H.
  now apply injective_projections.
  apply Rplus_le_le_0_compat ; apply Rle_0_sqr.
  apply Rle_refl.
Qed.

Lemma Cmod_ge_0 : forall x, 0 <= Cmod x.
Proof.
  intros x.
  apply sqrt_pos.
Qed.

Lemma Cmod_gt_0 :
  forall (x : C), x <> 0 <-> 0 < Cmod x.
Proof.
  intros x ; split; intro Hx.
  destruct (Cmod_ge_0 x); auto.
  apply sym_eq, Cmod_eq_0 in H. tauto.
  contradict Hx.
  apply Rle_not_lt, Req_le.
  rewrite Hx, Cmod_0; auto.
Qed.

Lemma Cmod_R : forall x : R, Cmod x = Rabs x.
Proof.
  intros x.
  unfold Cmod.
  simpl.
  rewrite Rmult_0_l, Rplus_0_r, Rmult_1_r.
  apply sqrt_Rsqr_abs.
Qed.

Lemma Cmod_inv : forall x : C, x <> 0 -> Cmod (/ x) = Rinv (Cmod x).
Proof.
  intros x Zx.
  apply Rmult_eq_reg_l with (Cmod x).
  rewrite <- Cmod_mult.
  rewrite Rinv_r.
  rewrite Cinv_r.
  rewrite Cmod_R.
  apply Rabs_R1.
  exact Zx.
  contradict Zx.
  now apply Cmod_eq_0.
  contradict Zx.
  now apply Cmod_eq_0.
Qed.

Lemma Cmod_div (x y : C) : y <> 0 -> Cmod (x / y) = Rdiv (Cmod x) (Cmod y).
Proof.
  intro Hy.
  unfold Cdiv.
  rewrite Cmod_mult.
  rewrite Cmod_inv; auto.
Qed.

Lemma Cmult_neq_0 (z1 z2 : C) : z1 <> 0 -> z2 <> 0 -> z1 * z2 <> 0.
Proof.
  intros Hz1 Hz2 Hz.
  assert (Cmod (z1 * z2) = 0).
  rewrite Hz, Cmod_0; auto.
  rewrite Cmod_mult in H.
  apply Rmult_integral in H ; destruct H.
  now apply Hz1, Cmod_eq_0.
  now apply Hz2, Cmod_eq_0.
Qed.

Lemma Cminus_eq_contra : forall r1 r2 : C, r1 <> r2 -> r1 - r2 <> 0.
Proof.
  intros ; contradict H ; apply injective_projections ;
  apply Rminus_diag_uniq.
  now apply (f_equal (@fst R R)) in H.
  now apply (f_equal (@snd R R)) in H.
Qed.

Lemma C_field_theory : field_theory (RtoC 0) (RtoC 1) Cplus Cmult Cminus Copp Cdiv Cinv eq.
Proof.
constructor.
constructor.
exact Cplus_0_l.
exact Cplus_comm.
exact Cplus_assoc.
exact Cmult_1_l.
exact Cmult_comm.
exact Cmult_assoc.
exact Cmult_plus_distr_r.
easy.
exact Cplus_opp_r.
intros H.
injection H.
exact R1_neq_R0.
easy.
apply Cinv_l.
Qed.

Add Field C_field_field : C_field_theory.

(*****************************************)
(** * Added Lemmas for QWIRE            **)
(*****************************************)

(** Notations *)

Notation C0 := (RtoC 0).
Notation C1 := (RtoC 1).
Notation C2 := (RtoC 2).

Lemma RtoC_pow : forall r n, (RtoC r) ^ n = RtoC (r ^ n).
Proof.
  intros.
  induction n.
  - reflexivity.
  - simpl.
    rewrite IHn.
    rewrite RtoC_mult.
    reflexivity.
Qed.

Lemma c_proj_eq : forall (c1 c2 : C), fst c1 = fst c2 -> snd c1 = snd c2 -> c1 = c2.
Proof. intros c1 c2 H1 H2. destruct c1, c2. simpl in *. subst. reflexivity. Qed.

Ltac lca := eapply c_proj_eq; simpl; lra.

Lemma Ci2 : Ci * Ci = -C1. Proof. lca. Qed.
Lemma Copp_mult_distr_r : forall c1 c2 : C, - (c1 * c2) = c1 * - c2.
Proof. intros; lca. Qed.
Lemma Copp_mult_distr_l : forall c1 c2 : C, - (c1 * c2) = - c1 * c2.
Proof. intros; lca. Qed.
Lemma Cplus_opp_l : forall c : C, - c + c = 0. Proof. intros; lca. Qed.
Lemma Cdouble : forall c : C, 2 * c = c + c. Proof. intros; lca. Qed.
Lemma Copp_involutive: forall c : C, - - c = c. Proof. intros; lca. Qed.

Lemma C0_imp : forall c : C, c <> 0 -> (fst c <> 0 \/ snd c <> 0)%R.
Proof. intros c H. destruct c. simpl.
       destruct (Req_EM_T r 0), (Req_EM_T r0 0); subst; intuition. Qed.
Lemma C0_fst_neq : forall (c : C), fst c <> 0 -> c <> 0.
Proof. intros c. intros N E. apply N. rewrite E. reflexivity. Qed.
Lemma C0_snd_neq : forall (c : C), snd c <> 0 -> c <> 0.
Proof. intros c. intros N E. apply N. rewrite E. reflexivity. Qed.
Lemma RtoC_neq : forall (r : R), r <> 0 -> RtoC r <> 0.
Proof. intros. apply C0_fst_neq. easy. Qed.

Lemma C1_neq_C0 : C1 <> C0.
Proof. apply C0_fst_neq.
       simpl.
       apply R1_neq_R0.
Qed.

Lemma nonzero_div_nonzero : forall c : C, c <> C0 -> / c <> C0.
Proof. intros.
       unfold not; intros.
        assert (H' : (c * (/ c) = c * C0)%C).
        { rewrite H0; easy. }
        rewrite Cinv_r in H'; try easy.
        rewrite Cmult_0_r in H'.
        apply C1_neq_C0; easy.
Qed.

Lemma eq_neg_implies_0 : forall (c : C),
  (-C1 * c)%C = c -> c = C0.
Proof.  intros.
        assert (H' : (- C1 * c + c = c + c)%C).
        { rewrite H; easy. }
        assert (H'' : (- C1 * c + c = C0)%C).
        { lca. }
        rewrite H'' in H'.
        assert (H0 : (c + c = C2 * c)%C). lca.
        rewrite H0 in H'.
        destruct (Ceq_dec c C0); try easy.
        assert (H1 : C2 <> C0).
        apply C0_fst_neq.
        simpl. lra.
        assert (H2 : (C2 * c)%C <> C0).
        apply Cmult_neq_0; try easy.
        rewrite <- H' in H2. easy.
Qed.

Lemma Cinv_mult_distr : forall c1 c2 : C, c1 <> 0 -> c2 <> 0 -> / (c1 * c2) = / c1 * / c2.
Proof.
  intros.
  apply c_proj_eq.
  - simpl.
    repeat rewrite Rmult_1_r.
    rewrite Rmult_div.
    rewrite Rmult_div.
    rewrite Rmult_opp_opp.
    unfold Rminus.
    rewrite <- RIneq.Ropp_div.
    rewrite <- Rdiv_plus_distr.
    rewrite Rmult_plus_distr_r.
    rewrite Rmult_plus_distr_l.
    apply Rdiv_cancel.
    lra.
    * apply Rsum_nonzero. apply C0_imp in H. assumption.
    * apply Rsum_nonzero. apply C0_imp in H0. assumption.
    * apply Rsum_nonzero. apply C0_imp in H. assumption.
    * apply Rsum_nonzero. apply C0_imp in H0. assumption.
  - simpl.
    repeat rewrite Rmult_1_r.
    rewrite Rmult_div.
    rewrite Rmult_div.
    unfold Rminus.
    rewrite <- Rdiv_plus_distr.
    repeat rewrite Rmult_plus_distr_r.
    repeat rewrite Rmult_plus_distr_l.
    repeat rewrite <- Ropp_mult_distr_r.
    repeat rewrite <- Ropp_mult_distr_l.
    repeat rewrite <- Ropp_plus_distr.
    apply Rdiv_cancel.
    lra.
    * apply Rsum_nonzero. apply C0_imp in H. assumption.
    * apply Rsum_nonzero. apply C0_imp in H0. assumption.
    * apply Rsum_nonzero. apply C0_imp in H. assumption.
    * apply Rsum_nonzero. apply C0_imp in H0. assumption.
Qed.

(* Lemmas about Cmod *)

Lemma Cmod_Cconj : forall c : C, Cmod (c^*) = Cmod c.
Proof.
  intro. unfold Cmod, Cconj. simpl.
  replace (- snd c * (- snd c * 1))%R with (snd c * (snd c * 1))%R by lra.
  easy.
Qed.

Lemma Cmod_real_pos :
  forall x : C,
    snd x = 0 ->
    fst x >= 0 ->
    x = Cmod x.
Proof.
  intros.
  unfold Cmod.
  rewrite H.
  replace (fst x ^ 2 + 0 ^ 2)%R with (fst x ^ 2)%R by lra.
  rewrite sqrt_pow2 by lra.
  destruct x; simpl in *.
  rewrite H.
  reflexivity.
Qed.

Lemma Cmod_sqr : forall c : C, (Cmod c ^2 = c^* * c)%C.
Proof.
  intro.
  rewrite RtoC_pow.
  simpl.
  rewrite Rmult_1_r.
  rewrite <- Cmod_Cconj at 1.
  rewrite <- Cmod_mult.
  rewrite Cmod_real_pos; auto.
  destruct c. simpl. lra.
  destruct c. simpl. nra.
Qed.

(* Lemmas about Conjugates *)

Lemma Cconj_R : forall r : R, r^* = r.         Proof. intros; lca. Qed.
Lemma Cconj_0 : 0^* = 0.                  Proof. lca. Qed.
Lemma Cconj_opp : forall C, (- C)^* = - (C^*). Proof. reflexivity. Qed.
Lemma Cconj_rad2 : (/ √2)^* = / √2.       Proof. lca. Qed.
Lemma Cplus_div2 : /2 + /2 = 1.           Proof. lca. Qed.
Lemma Cconj_involutive : forall c, (c^*)^* = c. Proof. intros; lca. Qed.
Lemma Cconj_plus_distr : forall (x y : C), (x + y)^* = x^* + y^*. Proof. intros; lca. Qed.
Lemma Cconj_mult_distr : forall (x y : C), (x * y)^* = x^* * y^*. Proof. intros; lca. Qed.

Lemma Cmult_conj_real : forall (c : C), snd (c * c^*) = 0.
Proof.
  intros c.
  unfold Cconj.
  unfold Cmult.
  simpl.
  rewrite <- Ropp_mult_distr_r.
  rewrite Rmult_comm.
  rewrite Rplus_opp_l.
  reflexivity.
Qed.

Lemma Cpow_nonzero : forall (r : R) (n : nat), (r <> 0 -> r ^ n <> C0)%C.
Proof.
  intros.
  rewrite RtoC_pow.
  apply C0_fst_neq.
  apply pow_nonzero.
  lra.
Qed.

(******************)
(** Square Roots **)
(******************)

Lemma Csqrt_sqrt : forall x : R, 0 <= x -> √ x * √ x = x.
Proof. intros. eapply c_proj_eq; simpl; try rewrite sqrt_sqrt; lra. Qed.

Lemma Csqrt2_sqrt : √ 2 * √ 2 = 2.
Proof. apply Csqrt_sqrt; lra. Qed.

Lemma Cinv_sqrt2_sqrt : /√2 * /√2 = /2.
Proof.
  eapply c_proj_eq; simpl; try lra.
  autorewrite with R_db.
  rewrite Rmult_assoc.
  rewrite (Rmult_comm (/2) _).
  repeat rewrite <- Rmult_assoc.
  rewrite sqrt_def; lra.
Qed.

Lemma Csqrt_inv : forall (r : R), 0 < r -> RtoC (√ (/ r)) = (/ √ r).
Proof.
  intros r H.
  apply c_proj_eq; simpl.
  field_simplify_eq [(pow2_sqrt r (or_introl H)) (sqrt_inv r H)].
  rewrite Rinv_r. reflexivity.
  apply sqrt_neq_0_compat; lra.
  apply sqrt_neq_0_compat; lra.
  field. apply sqrt_neq_0_compat; lra.
Qed.

Lemma Csqrt2_inv : RtoC (√ (/ 2)) = (/ √ 2).
Proof. apply Csqrt_inv; lra. Qed.

Lemma Csqrt_sqrt_inv : forall (r : R), 0 < r -> (√ r * √ / r) = 1.
Proof.
  intros.
  rewrite Csqrt_inv; trivial.
  rewrite Cinv_r; trivial.
  apply RtoC_neq.
  apply sqrt_neq_0_compat; easy.
Qed.

Lemma Csqrt2_sqrt2_inv : (√ 2 * √ / 2) = 1.
Proof. apply Csqrt_sqrt_inv. lra. Qed.

Lemma Csqrt2_inv_sqrt2 : ((√ / 2) * √ 2) = 1.
Proof. rewrite Cmult_comm. apply Csqrt2_sqrt2_inv. Qed.

Lemma Csqrt2_inv_sqrt2_inv : ((√ / 2) * (√ / 2)) = /2.
Proof.
  rewrite Csqrt2_inv. field_simplify.
  rewrite Csqrt2_sqrt. easy.
  apply RtoC_neq; lra.
  apply RtoC_neq; apply sqrt_neq_0_compat; lra.
Qed.

(****************************)
(** Complex Exponentiation **)
(****************************)

(* e^(iθ) *)
Definition Cexp (θ : R) : C := (cos θ, sin θ).

Lemma Cexp_0 : Cexp 0 = 1.
Proof. unfold Cexp. autorewrite with trig_db; easy. Qed.

Lemma Cexp_add: forall (x y : R), Cexp (x + y) = Cexp x * Cexp y.
Proof.
  intros.
  unfold Cexp.
  apply c_proj_eq; simpl.
  - apply cos_plus.
  - rewrite sin_plus. field.
Qed.

Lemma Cexp_neg : forall θ, Cexp (- θ) = / Cexp θ.
Proof.
  intros θ.
  unfold Cexp.
  rewrite sin_neg, cos_neg.
  apply c_proj_eq; simpl.
  - replace (cos θ * (cos θ * 1) + sin θ * (sin θ * 1))%R with
        (cos θ ^ 2 + sin θ ^ 2)%R by reflexivity.
    repeat rewrite <- Rsqr_pow2.
    rewrite Rplus_comm.
    rewrite sin2_cos2.
    field.
  - replace ((cos θ * (cos θ * 1) + sin θ * (sin θ * 1)))%R with
        (cos θ ^ 2 + sin θ ^ 2)%R by reflexivity.
    repeat rewrite <- Rsqr_pow2.
    rewrite Rplus_comm.
    rewrite sin2_cos2.
    field.
Qed.

Lemma Cexp_nonzero : forall θ, Cexp θ <> 0.
Proof.
  intro θ. unfold Cexp.
  specialize (cos_sin_0_var θ) as [? | ?].
  apply C0_fst_neq; auto.
  apply C0_snd_neq; auto.
Qed.

Lemma Cexp_mul_neg_l : forall θ, Cexp (- θ) * Cexp θ = 1.
Proof.
  unfold Cexp. intros θ.
  eapply c_proj_eq; simpl.
  - autorewrite with R_db trig_db.
    field_simplify_eq.
    repeat rewrite <- Rsqr_pow2.
    rewrite Rplus_comm.
    apply sin2_cos2.
  - autorewrite with R_db trig_db. field.
Qed.

Lemma Cexp_mul_neg_r : forall θ, Cexp θ * Cexp (-θ) = 1.
Proof. intros. rewrite Cmult_comm. apply Cexp_mul_neg_l. Qed.

Lemma Cexp_pow : forall θ k, Cexp θ ^ k = Cexp (θ * INR k).
Proof.
  intros.
  induction k.
  simpl. rewrite Rmult_0_r, Cexp_0. reflexivity.
  Local Opaque INR.
  simpl. rewrite IHk.
  rewrite <- Cexp_add.
  replace (S k) with (k + 1)%nat by lia.
  Local Transparent INR.
  rewrite plus_INR; simpl.
  apply f_equal. lra.
Qed.

Lemma Cmod_Cexp : forall θ, Cmod (Cexp θ) = 1.
Proof.
  intro. unfold Cexp, Cmod. simpl.
  replace ((cos θ * (cos θ * 1) + sin θ * (sin θ * 1)))%R
    with (cos θ * cos θ + sin θ * sin θ)%R by lra.
  specialize (sin2_cos2 θ) as H.
  unfold Rsqr in H.
  rewrite Rplus_comm in H.
  rewrite H. apply sqrt_1.
Qed.

Lemma Cmod_Cexp_alt : forall θ, Cmod (1 - Cexp (2 * θ)) = Cmod (2 * (sin θ)).
Proof.
  intro θ.
  unfold Cexp, Cminus, Cplus.
  simpl.
  unfold Cmod. simpl.
  apply f_equal.
  field_simplify_eq.
  unfold Rminus.
  rewrite (Rplus_assoc (_ ^ 2)).
  rewrite (Rplus_comm (- _)).
  rewrite <- Rplus_assoc.
  rewrite (Rplus_comm (_ ^ 2)).
  rewrite <- 2 Rsqr_pow2.
  rewrite sin2_cos2.
  rewrite cos_2a_sin.
  lra.
Qed.

(*****************************)
(** Cexp of multiples of PI **)
(*****************************)

(* Euler's Identity *)
Lemma Cexp_PI : Cexp PI = -1.
Proof. unfold Cexp. autorewrite with trig_db; easy. Qed.

Lemma Cexp_PI2 : Cexp (PI/2) = Ci.
Proof. unfold Cexp. autorewrite with trig_db; easy. Qed.

Lemma Cexp_2PI : Cexp (2 * PI) = 1.
Proof.
  unfold Cexp. rewrite sin_2PI, cos_2PI. reflexivity.
Qed.

Lemma Cexp_3PI2: Cexp (3 * PI / 2) = - Ci.
Proof.
  unfold Cexp.
  replace (3 * PI / 2)%R with (3 * (PI/2))%R by lra.
  rewrite cos_3PI2, sin_3PI2.
  lca.
Qed.

Lemma Cexp_PI4 : Cexp (PI / 4) = /√2 + /√2 * Ci.
Proof.
  unfold Cexp.
  rewrite sin_PI4, cos_PI4.
  eapply c_proj_eq; simpl.
  field_simplify_eq; trivial; apply sqrt2_neq_0.
  field_simplify_eq; trivial; apply sqrt2_neq_0.
Qed.

Lemma Cexp_PIm4 : Cexp (- PI / 4) = /√2 - /√2 * Ci.
Proof.
  unfold Cexp.
  rewrite Ropp_div.
  rewrite sin_antisym.
  rewrite cos_neg.
  rewrite sin_PI4, cos_PI4.
  eapply c_proj_eq; simpl.
  field_simplify_eq; trivial; apply sqrt2_neq_0.
  field_simplify_eq; trivial; apply sqrt2_neq_0.
Qed.

Lemma Cexp_0PI4 : Cexp (0 * PI / 4) = 1.
Proof. rewrite <- Cexp_0. apply f_equal. lra. Qed.

Lemma Cexp_1PI4 : Cexp (1 * PI / 4) = /√2 + /√2 * Ci.
Proof. rewrite <- Cexp_PI4. apply f_equal. lra. Qed.

Lemma Cexp_2PI4 : Cexp (2 * PI / 4) = Ci.
Proof. rewrite <- Cexp_PI2. apply f_equal. lra. Qed.

Lemma Cexp_3PI4 : Cexp (3 * PI / 4) = -/√2 + /√2 * Ci.
Proof.
  unfold Cexp.
  rewrite <- Rmult_div_assoc.
  rewrite cos_3PI4, sin_3PI4.
  eapply c_proj_eq; simpl.
  R_field_simplify; trivial. apply sqrt2_neq_0.
  R_field_simplify; trivial. apply sqrt2_neq_0.
Qed.

Lemma Cexp_4PI4 : Cexp (4 * PI / 4) = -1.
Proof. rewrite <- Cexp_PI. apply f_equal. lra. Qed.

Lemma Cexp_5PI4 : Cexp (5 * PI / 4) = -/√2 - /√2 * Ci.
Proof.
  unfold Cexp.
  rewrite <- Rmult_div_assoc.
  rewrite cos_5PI4, sin_5PI4.
  eapply c_proj_eq; simpl.
  R_field_simplify; trivial. apply sqrt2_neq_0.
  R_field_simplify; trivial. apply sqrt2_neq_0.
Qed.

Lemma Cexp_6PI4 : Cexp (6 * PI / 4) = -Ci.
Proof.
Proof. rewrite <- Cexp_3PI2. apply f_equal. lra. Qed.

Lemma Cexp_7PI4 : Cexp (7 * PI / 4) = /√2 - /√2 * Ci.
Proof.
  unfold Cexp.
  replace (7 * PI / 4)%R with (- PI / 4 + 2 * INR 1 * PI)%R.
  2:{ R_field_simplify. rewrite Rmult_1_r. lra. }
  rewrite cos_period, sin_period.
  rewrite Ropp_div.
  rewrite cos_neg, sin_neg.
  rewrite sin_PI4, cos_PI4.
  eapply c_proj_eq; simpl.
  R_field_simplify; trivial. apply sqrt2_neq_0.
  R_field_simplify; trivial. apply sqrt2_neq_0.
Qed.

Lemma Cexp_8PI4 : Cexp (8 * PI / 4) = 1.
Proof. rewrite <- Cexp_2PI. apply f_equal. lra. Qed.

(* This is a dramatically simplified version of Cexp_mod_2PI and we
   can probably get rid of it. *)
Lemma Cexp_PI4_m8 : forall (k : Z), Cexp (IZR (k - 8) * PI / 4) = Cexp (IZR k * PI / 4).
Proof.
  intros.
  unfold Rdiv.
  rewrite minus_IZR.
  unfold Rminus.
  repeat rewrite Rmult_plus_distr_r.
  replace (- (8) * PI * / 4)%R with (-(2 * PI))%R by lra.
  rewrite Cexp_add, Cexp_neg, Cexp_2PI.
  lca.
Qed.

Lemma Cexp_2nPI : forall (k : Z), Cexp (IZR (2 * k) * PI) = 1.
Proof.
  induction k using Z.peano_ind.
  - simpl. rewrite Rmult_0_l. apply Cexp_0.
  - rewrite Z.mul_succ_r.
    rewrite plus_IZR.
    rewrite Rmult_plus_distr_r.
    rewrite Cexp_add, Cexp_2PI.
    rewrite IHk.
    lca.
  - rewrite Z.mul_pred_r.
    rewrite minus_IZR.
    unfold Rminus.
    rewrite Rmult_plus_distr_r.
    rewrite <- Ropp_mult_distr_l.
    rewrite Cexp_add, Cexp_neg, Cexp_2PI.
    rewrite IHk.
    lca.
Qed.

Lemma Cexp_mod_2PI : forall (k : Z), Cexp (IZR k * PI) = Cexp (IZR (k mod 2) * PI).
Proof.
  intros.
  rewrite (Z.div_mod k 2) at 1 by lia.
  remember (k/2)%Z as k'.
  rewrite plus_IZR.
  rewrite Rmult_plus_distr_r.
  rewrite Cexp_add.
  rewrite Cexp_2nPI.
  lca.
Qed.

Lemma Cexp_mod_2PI_scaled : forall (k sc : Z),
  (sc <> 0)%Z ->
  Cexp (IZR k * PI / IZR sc) = Cexp (IZR (k mod (2 * sc)) * PI / IZR sc).
Proof.
  intros k sc H.
  rewrite (Z.div_mod k (2 * sc)) at 1 by lia.
  repeat rewrite plus_IZR.
  unfold Rdiv.
  repeat rewrite Rmult_plus_distr_r.
  rewrite Cexp_add.
  replace (IZR (2 * sc * (k / (2 * sc))) * PI * Rinv (IZR sc))%R with
      (IZR (2 * (k / (2 * sc))) * PI)%R.
  2:{ repeat rewrite mult_IZR.
      R_field_simplify.
      reflexivity.
      apply not_0_IZR; assumption. }
  rewrite Cexp_2nPI.
  lca.
Qed.

Hint Rewrite Cexp_0 Cexp_PI Cexp_PI2 Cexp_2PI Cexp_3PI2 Cexp_PI4 Cexp_PIm4
  Cexp_1PI4 Cexp_2PI4 Cexp_3PI4 Cexp_4PI4 Cexp_5PI4 Cexp_6PI4 Cexp_7PI4 Cexp_8PI4
  Cexp_add Cexp_neg : Cexp_db.

Opaque C.

(****************)
(** Automation **)
(****************)

Lemma Cminus_unfold : forall c1 c2, (c1 - c2 = c1 + -c2)%C. Proof. reflexivity. Qed.
Lemma Cdiv_unfold : forall c1 c2, (c1 / c2 = c1 */ c2)%C. Proof. reflexivity. Qed.

(* For proving goals of the form x <> 0 or 0 < x *)
Ltac nonzero :=
  repeat split;
   try match goal with
       | |- not (@eq _ _ (RtoC (IZR Z0))) => apply RtoC_neq
       | |- not (@eq _ (Cpow _ _) (RtoC (IZR Z0))) => apply Cpow_nonzero; try apply RtoC_neq
       | |- not (@eq _ Ci (RtoC (IZR Z0))) => apply C0_snd_neq; simpl
       | |- not (@eq _ (Cexp _) (RtoC (IZR Z0))) => apply Cexp_nonzero
       end;
  repeat
    match goal with
    | |- not (@eq _ (sqrt (pow _ _)) (IZR Z0)) => rewrite sqrt_pow
    | |- not (@eq _ (pow _ _) (IZR Z0)) => apply pow_nonzero; try apply RtoC_neq
    | |- not (@eq _ (sqrt _) (IZR Z0)) => apply sqrt_neq_0_compat
    | |- not (@eq _ (Rinv _) (IZR Z0)) => apply Rinv_neq_0_compat
    | |- not (@eq _ (Rmult _ _) (IZR Z0)) => apply Rmult_integral_contrapositive_currified
    end;
  repeat
    match goal with
    | |- Rlt (IZR Z0) (Rmult _ _) => apply Rmult_lt_0_compat
    | |- Rlt (IZR Z0) (Rinv _) => apply Rinv_0_lt_compat
    | |- Rlt (IZR Z0) (pow _ _) => apply pow_lt
    end; match goal with
         | |- not (@eq _ _ _) => lra
         | |- Rlt _ _ => lra
         | |- Rle _ _ => lra
         end.

Hint Rewrite Cminus_unfold Cdiv_unfold Ci2 Cconj_R Cconj_opp Cconj_rad2
     Cinv_sqrt2_sqrt Cplus_div2
     Cplus_0_l Cplus_0_r Cplus_opp_r Cplus_opp_l Copp_0  Copp_involutive
     Cmult_0_l Cmult_0_r Cmult_1_l Cmult_1_r : C_db.

Hint Rewrite <- Copp_mult_distr_l Copp_mult_distr_r Cdouble : C_db.
Hint Rewrite Csqrt_sqrt using Psatz.lra : C_db.
Hint Rewrite Cinv_l Cinv_r using nonzero : C_db.
(* Previously in the other direction *)
Hint Rewrite Cinv_mult_distr using nonzero : C_db.

(* Light rewriting db *)
Hint Rewrite Cplus_0_l Cplus_0_r Cmult_0_l Cmult_0_r Copp_0
             Cconj_R Cmult_1_l Cmult_1_r : C_db_light.

(* Distributing db *)
Hint Rewrite Cmult_plus_distr_l Cmult_plus_distr_r Copp_plus_distr Copp_mult_distr_l
              Copp_involutive : Cdist_db.

Ltac Csimpl :=
  repeat match goal with
  | _ => rewrite Cmult_0_l
  | _ => rewrite Cmult_0_r
  | _ => rewrite Cplus_0_l
  | _ => rewrite Cplus_0_r
  | _ => rewrite Cmult_1_l
  | _ => rewrite Cmult_1_r
  | _ => rewrite Cconj_R
  end.

Ltac C_field_simplify := repeat field_simplify_eq [ Csqrt2_sqrt Csqrt2_inv Ci2].
Ltac C_field := C_field_simplify; nonzero; trivial.

Ltac has_term t exp  :=
  match exp with
    | context[t] => idtac
  end.

Ltac group_radicals :=
  repeat rewrite Cconj_opp;
  repeat rewrite Cconj_rad2;
  repeat rewrite <- Copp_mult_distr_l;
  repeat rewrite <- Copp_mult_distr_r;
  repeat match goal with
  | _ => rewrite Cinv_sqrt2_sqrt
  | |- context [ ?x * ?y ] => tryif has_term (√ 2) x then fail
                            else (has_term (√ 2) y; rewrite (Cmult_comm x y))
  | |- context [ ?x * ?y * ?z ] =>
    tryif has_term (√ 2) y then fail
    else (has_term (√ 2) x; has_term (√ 2) z; rewrite <- (Cmult_assoc x y z))
  | |- context [ ?x * (?y * ?z) ] =>
    has_term (√ 2) x; has_term (√ 2) y; rewrite (Cmult_assoc x y z)
  end.

Ltac cancel_terms t :=
  repeat rewrite Cmult_plus_distr_l;
  repeat rewrite Cmult_plus_distr_r;
  repeat match goal with
  | _ => rewrite Cmult_1_l
  | _ => rewrite Cmult_1_r
  | _ => rewrite Cinv_r; try nonzero
  | _ => rewrite Cinv_l; try nonzero
  | |- context[(?x * ?y)%C]        => tryif has_term (/ t)%C y then fail else has_term (/ t)%C x; has_term t y;
                                    rewrite (Cmult_comm x y)
  | |- context[(?x * (?y * ?z))%C] => has_term t x; has_term (/ t)%C y;
                                    rewrite (Cmult_assoc x y z)
  | |- context[(?x * (?y * ?z))%C] => tryif has_term t y then fail else has_term t x; has_term (/ t)%C z;
                                    rewrite (Cmult_comm y z)
  | |- context[(?x * ?y * ?z)%C]   => tryif has_term t x then fail else has_term t y; has_term (/ t)%C z;
                                    rewrite <- (Cmult_assoc x y z)
  end.

Ltac group_Cexp :=
  repeat rewrite <- Cexp_neg;
  repeat match goal  with
  | _ => rewrite <- Cexp_add
  | |- context [ ?x * Cexp ?y ] => rewrite (Cmult_comm x (Cexp y))
  | |- context [ ?x * (?y * ?z) ] => rewrite Cmult_assoc
  end.

author: inQWIRE

repo: Stabilizer-Types


text:
Require Import Fiat.Common Coq.Arith.Arith Coq.Bool.Bool Coq.Sets.Ensembles.

Class DecideableEnsemble {A} (P : Ensemble A) :=
  { dec : A -> bool;
    dec_decides_P : forall a, dec a = true <-> P a}.

Lemma Decides_false {A} :
  forall (P : Ensemble A)
         (P_dec : DecideableEnsemble P) a,
    dec a = false <-> ~ (P a).
Proof.
  split; unfold not; intros.
  + apply dec_decides_P in H0; congruence.
  + case_eq (dec a); intros; eauto.
    apply dec_decides_P in H0; intuition.
Qed.

#[global]
Program Instance DecideableEnsemble_gt {A} (f f' : A -> nat)
  : DecideableEnsemble (fun a => f a > f' a) :=
  {| dec a := if le_lt_dec (f a) (f' a) then false else true |}.
Next Obligation.
  intros; find_if_inside; intuition.
Defined.

#[global]
Program Instance DecideableEnsemble_And
         {A : Type}
         {P P' : Ensemble A}
         {P_dec : DecideableEnsemble P}
         {P'_dec : DecideableEnsemble P'}
: DecideableEnsemble (fun a => P a /\ P' a) :=
  {| dec a := (@dec _ _ P_dec a) && (@dec _ _  P'_dec a) |}.
Next Obligation.
  intros; rewrite <- (@dec_decides_P _ P),
          <- (@dec_decides_P _ P').
  setoid_rewrite andb_true_iff; reflexivity.
Defined.

(* Class used to overload equality test notation (==) in queries. *)
Class Query_eq (A : Type) :=
      {A_eq_dec : forall a a' : A, {a = a'} + {a <> a'}}.

Infix "==" := (A_eq_dec) (at level 1).

#[global]
Instance Query_eq_nat : Query_eq nat :=
  {| A_eq_dec := eq_nat_dec |}.

#[global]
Instance Query_eq_bool : Query_eq bool :=
  {| A_eq_dec := bool_dec |}.

#[global]
Instance Query_eq_list {A}
         (_ : Query_eq A)
  : Query_eq (list A) :=
  {| A_eq_dec := List.list_eq_dec A_eq_dec |}.

#[global]
Program Instance DecideableEnsemble_NEqDec
         {A B : Type}
         {b_eq_dec : Query_eq B}
         (f f' : A -> B)
: DecideableEnsemble (fun a : A => f a <> f' a) :=
  {| dec a := if A_eq_dec (f a) (f' a) then false else true |}.
Next Obligation.
  intros; find_if_inside; intuition.
Defined.

#[global]
Program Instance DecideableEnsemble_EqDec {A B : Type}
         (B_eq_dec : Query_eq B)
         (f f' : A -> B)
: DecideableEnsemble (fun a => eq (f a) (f' a)) :=
  {| dec a := if A_eq_dec (f a) (f' a) then true else false |}.
Next Obligation.
  intros; find_if_inside; split; congruence.
Defined.

#[global]
Program Instance DecideableEnsemble_Not
         {A : Type}
         (P : Ensemble A)
         {P_dec : DecideableEnsemble P}
: DecideableEnsemble (fun a => ~ P a) :=
  {| dec a := negb (dec a) |}.
Next Obligation.
  intros; case_eq (dec a); intros; intuition eauto.
  - discriminate.
  - rewrite dec_decides_P in H; intuition.
  - rewrite <- dec_decides_P in H1; congruence.
Defined.

#[global]
Program Instance DecideableEnsemble_True
         {A : Type}
: DecideableEnsemble (fun a : A => True) :=
  {| dec a := true |}.
Next Obligation.
  intros; intuition eauto.
Defined.

#[global]
Program Instance DecideableEnsemble_False
         {A : Type}
: DecideableEnsemble (fun a : A => False) :=
  {| dec a := false |}.
Next Obligation.
  intros; intuition eauto; discriminate.
Defined.

#[global]
Program Instance DecideableEnsemble_Or
         {A : Type}
         (P P' : Ensemble A)
         {P_dec : DecideableEnsemble P}
         {P'_dec : DecideableEnsemble P'}
: DecideableEnsemble (fun a : A => P a \/ P' a) :=
  {| dec a := if dec (P := P) a then true else dec (P := P') a |}.
Next Obligation.
  intros; case_eq (dec (P := P) a);
  [ rewrite dec_decides_P | rewrite Decides_false];
  intuition.
  setoid_rewrite dec_decides_P in H0; intuition.
  setoid_rewrite dec_decides_P; intuition.
Defined.

author: mit-plv

repo: fiat

save_path: github-repos/coq/mit-plv-fiat


text:
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU Lesser General Public License as        *)
(*  published by the Free Software Foundation, either version 2.1 of   *)
(*  the License, or  (at your option) any later version.               *)
(*  This file is also distributed under the terms of the               *)
(*  INRIA Non-Commercial License Agreement.                            *)
(*                                                                     *)
(* *********************************************************************)

(* A solver for unification constraints. *)

Require Import Recdef Coqlib Maps Errors.

Local Open Scope nat_scope.
Local Open Scope error_monad_scope.

(** This module provides a solver for sets of unification constraints of the
  following kinds: [T(x) = base-type] or [T(x) = T(y)].
  The unknowns are the types [T(x)] of every identifier [x]. *)

(** The interface for base types. *)

Module Type TYPE_ALGEBRA.

Parameter t: Type.
Parameter eq: forall (x y: t), {x=y} + {x<>y}.
Parameter default: t.

End TYPE_ALGEBRA.

(** The constraint solver. *)

Module UniSolver (T: TYPE_ALGEBRA).

(* The current set of constraints is represented by a record with two components:
- [te_typ]: a partial map from variables to types
- [te_equ]: a list of pairs [(x,y)] of variables, indicating that
  the type of [x] must be equal to the type of [y].
*)

Definition constraint : Type := (positive * positive)%type.

Record typenv : Type := Typenv {
  te_typ: PTree.t T.t;       (**r mapping var -> typ *)
  te_equ: list constraint    (**r additional equality constraints *)
}.

Definition initial : typenv := {| te_typ := PTree.empty _; te_equ := nil |}.

(** Add the constraint [T(x) = ty]. *)

Definition set (e: typenv) (x: positive) (ty: T.t) : res typenv :=
  match e.(te_typ)!x with
  | None =>
      OK {| te_typ := PTree.set x ty e.(te_typ);
            te_equ := e.(te_equ) |}
  | Some ty' =>
      if T.eq ty ty'
      then OK e
      else Error (MSG "bad definition/use of variable " :: POS x :: nil)
  end.

Fixpoint set_list (e: typenv) (rl: list positive) (tyl: list T.t) {struct rl}: res typenv :=
  match rl, tyl with
  | nil, nil => OK e
  | r1::rs, ty1::tys => do e1 <- set e r1 ty1; set_list e1 rs tys
  | _, _ => Error (msg "arity mismatch")
  end.

(** Add the constraint [T(x) = T(y)].
    The boolean result is [true] if the types of [x] or [y] could be
    made more precise.  Otherwise, [te_typ] does not change and
    [false] is returned. *)

Definition move (e: typenv) (r1 r2: positive) : res (bool * typenv) :=
  if peq r1 r2 then OK (false, e) else
  match e.(te_typ)!r1, e.(te_typ)!r2 with
  | None, None =>
      OK (false, {| te_typ := e.(te_typ); te_equ := (r1, r2) :: e.(te_equ) |})
  | Some ty1, None =>
      OK (true, {| te_typ := PTree.set r2 ty1 e.(te_typ); te_equ := e.(te_equ) |})
  | None, Some ty2 =>
      OK (true, {| te_typ := PTree.set r1 ty2 e.(te_typ); te_equ := e.(te_equ) |})
  | Some ty1, Some ty2 =>
      if T.eq ty1 ty2
      then OK (false, e)
      else Error(MSG "ill-typed move from " :: POS r1 :: MSG " to " :: POS r2 :: nil)
  end.

(** Solve the remaining subtyping constraints by iteration. *)

Fixpoint solve_rec (e: typenv) (changed: bool) (q: list constraint) : res (typenv * bool) :=
  match q with
  | nil =>
      OK (e, changed)
  | (r1, r2) :: q' =>
      do (changed1, e1) <- move e r1 r2; solve_rec e1 (changed || changed1) q'
  end.

(** Measuring the state *)

Lemma move_shape:
  forall e r1 r2 changed e',
  move e r1 r2 = OK (changed, e') ->
  (e'.(te_equ) = e.(te_equ) \/ e'.(te_equ) = (r1, r2) :: e.(te_equ))
  /\ (changed = true -> e'.(te_equ) = e.(te_equ)).
Proof.
  unfold move; intros.
  destruct (peq r1 r2). inv H. auto.
  destruct e.(te_typ)!r1 as [ty1|]; destruct e.(te_typ)!r2 as [ty2|]; inv H; simpl.
  destruct (T.eq ty1 ty2); inv H1. auto.
  auto.
  auto.
  split. auto. intros. discriminate.
Qed.

Lemma length_move:
  forall e r1 r2 changed e',
  move e r1 r2 = OK (changed, e') ->
  length e'.(te_equ) + (if changed then 1 else 0) <= S(length e.(te_equ)).
Proof.
  unfold move; intros.
  destruct (peq r1 r2). inv H. lia.
  destruct e.(te_typ)!r1 as [ty1|]; destruct e.(te_typ)!r2 as [ty2|]; inv H; simpl.
  destruct (T.eq ty1 ty2); inv H1. lia.
  lia.
  lia.
  lia.
Qed.

Lemma length_solve_rec:
  forall q e ch e' ch',
  solve_rec e ch q = OK (e', ch') ->
  length e'.(te_equ) + (if ch' && negb ch then 1 else 0) <= length e.(te_equ) + length q.
Proof.
  induction q; simpl; intros.
- inv H. replace (ch' && negb ch') with false. lia. destruct ch'; auto.
- destruct a as [r1 r2]; monadInv H. rename x0 into e0. rename x into ch0.
  exploit IHq; eauto. intros A.
  exploit length_move; eauto. intros B.
  set (X := (if ch' && negb (ch || ch0) then 1 else 0)) in *.
  set (Y := (if ch0 then 1 else 0)) in *.
  set (Z := (if ch' && negb ch then 1 else 0)) in *.
  cut (Z <= X + Y). intros. lia.
  unfold X, Y, Z. destruct ch'; destruct ch; destruct ch0; simpl; auto.
Qed.

Definition weight_typenv (e: typenv) : nat := length e.(te_equ).

(** Iterative solving of the remaining constraints *)

Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv :=
  match solve_rec {| te_typ := e.(te_typ); te_equ := nil |} false e.(te_equ) with
  | OK(e', false) => OK e                   (**r no more changes, fixpoint reached *)
  | OK(e', true)  => solve_constraints e'   (**r one more iteration *)
  | Error msg => Error msg
  end.
Proof.
  intros. exploit length_solve_rec; eauto. simpl. intros.
  unfold weight_typenv. lia.
Qed.

Definition typassign := positive -> T.t.

Definition makeassign (e: typenv) : typassign :=
  fun x => match e.(te_typ)!x with Some ty => ty | None => T.default end.

Definition solve (e: typenv) : res typassign :=
  do e' <- solve_constraints e; OK(makeassign e').

(** What it means to be a solution *)

Definition satisf (te: typassign) (e: typenv) : Prop :=
   (forall x ty, e.(te_typ)!x = Some ty -> te x = ty)
/\ (forall x y, In (x, y) e.(te_equ) -> te x = te y).

Lemma satisf_initial: forall te, satisf te initial.
Proof.
  unfold initial; intros; split; simpl; intros.
  rewrite PTree.gempty in H; discriminate.
  contradiction.
Qed.

(** Soundness proof *)

Lemma set_incr:
  forall te x ty e e', set e x ty = OK e' -> satisf te e' -> satisf te e.
Proof.
  unfold set; intros. destruct (te_typ e)!x as [ty'|] eqn:E.
- destruct (T.eq ty ty'); inv H. auto.
- inv H. destruct H0 as [A B]; simpl in *. red; split; intros; auto.
  apply A. rewrite PTree.gso by congruence. auto.
Qed.

Global Hint Resolve set_incr: ty.

Lemma set_sound:
  forall te x ty e e', set e x ty = OK e' -> satisf te e' -> te x = ty.
Proof.
  unfold set; intros. destruct H0 as [P Q].
  destruct (te_typ e)!x as [ty'|] eqn:E.
- destruct (T.eq ty ty'); inv H. eauto.
- inv H. simpl in P. apply P. apply PTree.gss.
Qed.

Lemma set_list_incr:
  forall te xl tyl e e', set_list e xl tyl = OK e' -> satisf te e' -> satisf te e.
Proof.
  induction xl; destruct tyl; simpl; intros; monadInv H; eauto with ty.
Qed.

Global Hint Resolve set_list_incr: ty.

Lemma set_list_sound:
  forall te xl tyl e e', set_list e xl tyl = OK e' -> satisf te e' -> map te xl = tyl.
Proof.
  induction xl; destruct tyl; simpl; intros; monadInv H.
  auto.
  f_equal. eapply set_sound; eauto with ty. eauto.
Qed.

Lemma move_incr:
  forall te e r1 r2 e' changed,
  move e r1 r2 = OK(changed, e') -> satisf te e' -> satisf te e.
Proof.
  unfold move; intros. destruct H0 as [P Q].
  destruct (peq r1 r2). inv H; split; auto.
  destruct (te_typ e)!r1 as [ty1|] eqn:E1;
  destruct (te_typ e)!r2 as [ty2|] eqn:E2.
- destruct (T.eq ty1 ty2); inv H. split; auto.
- inv H; simpl in *; split; auto. intros. apply P.
  rewrite PTree.gso by congruence. auto.
- inv H; simpl in *; split; auto. intros. apply P.
  rewrite PTree.gso by congruence. auto.
- inv H; simpl in *; split; auto.
Qed.

Global Hint Resolve move_incr: ty.

Lemma move_sound:
  forall te e r1 r2 e' changed,
  move e r1 r2 = OK(changed, e') -> satisf te e' -> te r1 = te r2.
Proof.
  unfold move; intros. destruct H0 as [P Q].
  destruct (peq r1 r2). congruence.
  destruct (te_typ e)!r1 as [ty1|] eqn:E1;
  destruct (te_typ e)!r2 as [ty2|] eqn:E2.
- destruct (T.eq ty1 ty2); inv H. erewrite ! P by eauto. auto.
- inv H; simpl in *. rewrite (P r1 ty1). rewrite (P r2 ty1). auto.
  apply PTree.gss. rewrite PTree.gso by congruence. auto.
- inv H; simpl in *. rewrite (P r1 ty2). rewrite (P r2 ty2). auto.
  rewrite PTree.gso by congruence. auto. apply PTree.gss.
- inv H; simpl in *. apply Q; auto.
Qed.

Lemma solve_rec_incr:
  forall te q e changed e' changed',
  solve_rec e changed q = OK(e', changed') -> satisf te e' -> satisf te e.
Proof.
  induction q; simpl; intros.
- inv H. auto.
- destruct a as [r1 r2]; monadInv H. eauto with ty.
Qed.

Lemma solve_rec_sound:
  forall te r1 r2 q e changed e' changed',
  solve_rec e changed q = OK(e', changed') -> In (r1, r2) q -> satisf te e' ->
  te r1 = te r2.
Proof.
  induction q; simpl; intros.
- contradiction.
- destruct a as [r3 r4]; monadInv H. destruct H0.
  + inv H. eapply move_sound; eauto. eapply solve_rec_incr; eauto.
  + eapply IHq; eauto with ty.
Qed.

Lemma move_false:
  forall e r1 r2 e',
  move e r1 r2 = OK(false, e') ->
  te_typ e' = te_typ e /\ makeassign e r1 = makeassign e r2.
Proof.
  unfold move; intros.
  destruct (peq r1 r2). inv H. split; auto.
  unfold makeassign;
  destruct (te_typ e)!r1 as [ty1|] eqn:E1;
  destruct (te_typ e)!r2 as [ty2|] eqn:E2.
- destruct (T.eq ty1 ty2); inv H. auto.
- discriminate.
- discriminate.
- inv H. split; auto.
Qed.

Lemma solve_rec_false:
  forall r1 r2 q e changed e',
  solve_rec e changed q = OK(e', false) ->
  changed = false /\
  (In (r1, r2) q -> makeassign e r1 = makeassign e r2).
Proof.
  induction q; simpl; intros.
- inv H. tauto.
- destruct a as [r3 r4]; monadInv H.
  exploit IHq; eauto. intros [P Q].
  destruct changed; try discriminate. destruct x; try discriminate.
  exploit move_false; eauto. intros [U V].
  split. auto. intros [A|A]. inv A. auto. exploit Q; auto.
  unfold makeassign; rewrite U; auto.
Qed.

Lemma solve_constraints_incr:
  forall te e e', solve_constraints e = OK e' -> satisf te e' -> satisf te e.
Proof.
  intros te e; functional induction (solve_constraints e); intros.
- inv H. auto.
- exploit solve_rec_incr; eauto. intros [A B].
  split; auto. intros; eapply solve_rec_sound; eauto.
- discriminate.
Qed.

Lemma solve_constraints_sound:
  forall e e', solve_constraints e = OK e' -> satisf (makeassign e') e'.
Proof.
  intros e0; functional induction (solve_constraints e0); intros.
- inv H. split; intros.
  unfold makeassign; rewrite H. split; auto with ty.
  exploit solve_rec_false. eauto. intros [A B]. eapply B; eauto.
- eauto.
- discriminate.
Qed.

Theorem solve_sound:
  forall e te, solve e = OK te -> satisf te e.
Proof.
  unfold solve; intros. monadInv H.
  eapply solve_constraints_incr. eauto. eapply solve_constraints_sound; eauto.
Qed.

(** Completeness proof *)

Lemma set_complete:
  forall te e x ty,
  satisf te e -> te x = ty -> exists e', set e x ty = OK e' /\ satisf te e'.
Proof.
  unfold set; intros. generalize H; intros [P Q].
  destruct (te_typ e)!x as [ty1|] eqn:E.
- replace ty1 with ty. rewrite dec_eq_true. exists e; auto.
  exploit P; eauto. congruence.
- econstructor; split; eauto. split; simpl; intros; auto.
  rewrite PTree.gsspec in H1. destruct (peq x0 x). congruence. eauto.
Qed.

Lemma set_list_complete:
  forall te xl tyl e,
  satisf te e -> map te xl = tyl ->
  exists e', set_list e xl tyl = OK e' /\ satisf te e'.
Proof.
  induction xl; intros; inv H0; simpl.
  econstructor; eauto.
  exploit (set_complete te e a (te a)); auto. intros (e1 & P & Q).
  exploit (IHxl (map te xl) e1); auto. intros (e2 & U & V).
  exists e2; split; auto. rewrite P; auto.
Qed.

Lemma move_complete:
  forall te e r1 r2,
  satisf te e -> te r1 = te r2 ->
  exists changed e', move e r1 r2 = OK(changed, e') /\ satisf te e'.
Proof.
  unfold move; intros. elim H; intros P Q.
  assert (Q': forall x y, In (x, y) ((r1, r2) :: te_equ e) -> te x = te y).
  { intros. destruct H1; auto. congruence. }
  destruct (peq r1 r2). econstructor; econstructor; eauto.
  destruct (te_typ e)!r1 as [ty1|] eqn:E1;
  destruct (te_typ e)!r2 as [ty2|] eqn:E2.
- replace ty2 with ty1. rewrite dec_eq_true. econstructor; econstructor; eauto.
  exploit (P r1); eauto. exploit (P r2); eauto. congruence.
- econstructor; econstructor; split; eauto.
  split; simpl; intros; auto. rewrite PTree.gsspec in H1. destruct (peq x r2).
  inv H1. rewrite <- H0. eauto.
  eauto.
- econstructor; econstructor; split; eauto.
  split; simpl; intros; auto. rewrite PTree.gsspec in H1. destruct (peq x r1).
  inv H1. rewrite H0. eauto.
  eauto.
- econstructor; econstructor; split; eauto.
  split; eauto.
Qed.

Lemma solve_rec_complete:
  forall te q e changed,
  satisf te e ->
  (forall r1 r2, In (r1, r2) q -> te r1 = te r2) ->
  exists e' changed', solve_rec e changed q = OK(e', changed') /\ satisf te e'.
Proof.
  induction q; simpl; intros.
- econstructor; econstructor; eauto.
- destruct a as [r1 r2].
  exploit (move_complete te e r1 r2); auto. intros (changed1 & e1 & A & B).
  exploit (IHq e1 (changed || changed1)); auto. intros (e' & changed' & C & D).
  exists e'; exists changed'. rewrite A; simpl; rewrite C; auto.
Qed.

Lemma solve_constraints_complete:
  forall te e, satisf te e -> exists e', solve_constraints e = OK e' /\ satisf te e'.
Proof.
  intros te e. functional induction (solve_constraints e); intros.
- exists e; auto.
- exploit (solve_rec_complete te (te_equ e) {| te_typ := te_typ e; te_equ := nil |} false).
  destruct H; split; auto. simpl; tauto.
  destruct H; auto.
  intros (e1 & changed1 & P & Q).
  apply IHr. congruence.
- exploit (solve_rec_complete te (te_equ e) {| te_typ := te_typ e; te_equ := nil |} false).
  destruct H; split; auto. simpl; tauto.
  destruct H; auto.
  intros (e1 & changed1 & P & Q).
  congruence.
Qed.

Lemma solve_complete:
  forall te e, satisf te e -> exists te', solve e = OK te'.
Proof.
  intros. unfold solve.
  destruct (solve_constraints_complete te e H) as (e' & P & Q).
  econstructor. rewrite P. simpl. eauto.
Qed.

End UniSolver.

author: AbsInt

repo: CompCert

save_path: github-repos/coq/AbsInt-CompCert


text:
(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
(*    AtomicJl:
        Decidable, Tag-Based (Atomically) Semantic Subtyping
        for Nominal Types, Pairs, and Unions.  *)

(** * AtomicJl: Propositions about Reductive Subtyping *)
(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)

Add LoadPath "../..". (* root directory of the repo *)

Require Import Mechanization.Aux.Identifier.

Require Import Mechanization.AtomicJl.BaseDefs.
Require Import Mechanization.AtomicJl.BaseProps.
Require Import Mechanization.AtomicJl.MatchProps.

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Arith.Arith.
Require Import Coq.Bool.Bool.

Close Scope btj_scope.
Open  Scope btjm_scope.
Open  Scope btjnf_scope.
Open  Scope btjr_scope.

(* ################################################################# *)
(** ** Auxiliary Statements *)
(* ################################################################# *)

(* ================================================================= *)
(** *** Union of Normal Form *)
(* ================================================================= *)

(* DEP: mk_nf_nf__equal *)
Lemma union_nf_sub_r__components_sub_r : forall (t1 t2 t' : ty),
    |- TUnion t1 t2 << t' ->
    InNF(t1) -> InNF(t2) ->
    |- t1 << t' /\ |- t2 << t'.
Proof.
  intros t1 t2 t' H. remember (TUnion t1 t2) as t eqn:Heq.
  induction H; intros Hnf1 Hnf2; try solve [inversion Heq].
  - (* UnionL *)
    inversion Heq; subst. split; assumption.
  - (* UnionR1 *)
    inversion Heq; subst. specialize (IHsub_r H0).
    split; (apply SR_UnionR1 || apply SR_UnionR2); tauto.
  - (* UnionR2 *)
    inversion Heq; subst. specialize (IHsub_r H0).
    split; (apply SR_UnionR2 || apply SR_UnionR2); tauto.
  - (* NF *)
    subst. simpl in *. apply IHsub_r; try assumption.
    rewrite (mk_nf_nf__equal _ Hnf1).
    rewrite (mk_nf_nf__equal _ Hnf2).
    reflexivity.
Qed.

(* ================================================================= *)
(** *** About [unite_pairs] *)
(* ================================================================= *)

(* DEP: sub_r__rflxv, unite_pairs_t_union, unite_pairs_union_t,
        union_in_nf__components_in_nf,
        mk_nf_nf__equal, mk_nf__in_nf *)
Lemma unite_pairs_of_nf__preserves_sub_r : forall (t1 t2 t1' t2' : ty),
    |- t1 << t1' ->
    |- t2 << t2' ->
    InNF(t1) -> InNF(t1') ->
    InNF(t2) -> InNF(t2') ->
    |- unite_pairs t1 t2 << unite_pairs t1' t2'.
Proof.
  intros ta tb ta' tb' Hsub1.
  generalize dependent tb'. generalize dependent tb.
  induction Hsub1; intros tb tb' Hsub2;
    try solve [
          induction Hsub2; intros Hnfa Hnfa' Hnfb Hnfb';
          try solve [
                simpl; constructor; constructor; assumption
              (* UnionL *)
              | rewrite unite_pairs_t_union; try resolve_not_union;
                destruct (union_in_nf__components_in_nf _ _ Hnfb) as [Hnfb1 Hnfb2];
                constructor; [apply IHHsub2_1 | apply IHHsub2_2];
                assumption || constructor
              (* UnionR1 *)
              | rewrite unite_pairs_t_union; try resolve_not_union;
                destruct (union_in_nf__components_in_nf _ _ Hnfb') as [Hnfb1 Hnfb2];
                apply SR_UnionR1; apply IHHsub2; assumption || constructor
              (* UnionR2 *)
              | rewrite unite_pairs_t_union; try resolve_not_union;
                destruct (union_in_nf__components_in_nf _ _ Hnfb') as [Hnfb1 Hnfb2];
                apply SR_UnionR2; apply IHHsub2; assumption || constructor
              (* NF *)
              | rewrite <- (mk_nf_nf__equal _ Hnfb);
                apply IHHsub2; try assumption; apply mk_nf__in_nf ]
        ].
  - (* UnionL, tb *)
    intros Hnfa Hnfa' Hnfb Hnfb'. rewrite unite_pairs_union_t.
    destruct (union_in_nf__components_in_nf _ _ Hnfa) as [Hnfa1 Hnfa2].
    constructor; [apply IHHsub1_1 | apply IHHsub1_2]; assumption.
  - (* UnionR1, tb *)
    intros Hnfa Hnfa' Hnfb Hnfb'. rewrite unite_pairs_union_t.
    destruct (union_in_nf__components_in_nf _ _ Hnfa') as [Hnfa1 Hnfa2].
    apply SR_UnionR1; apply IHHsub1; assumption.
  - (* UnionR2, tb *)
    intros Hnfa Hnfa' Hnfb Hnfb'. rewrite unite_pairs_union_t.
    destruct (union_in_nf__components_in_nf _ _ Hnfa') as [Hnfa1 Hnfa2].
    apply SR_UnionR2; apply IHHsub1; assumption.
  - (* NF, tb *)
    intros Hnfa Hnfa' Hnfb Hnfb'.
    rewrite <- (mk_nf_nf__equal _ Hnfa).
    apply IHHsub1; try assumption. apply mk_nf__in_nf.
Qed.

(* DEP: unite_pairs_t_union, unite_pairs_union_t,
        union_in_nf__components_in_nf, union_nf_sub_r__components_sub_r *)
Lemma unite_pairs_of_nf__preserves_sub_r1 : forall (t1 t2 t1' t2' : ty),
    InNF(t1) -> |- t1 << t1' ->
    InNF(t2) -> |- t2 << t2' ->
    |- unite_pairs t1 t2 << TPair t1' t2'.
Proof.
  intros ta; induction ta;
    intros tb; induction tb;
      intros ta' tb' Hnf1 Hsub1 Hnf2 Hsub2;
      try solve [
            simpl; constructor; assumption
          | match goal with
            | [Hnf1: InNF(?t), Hnf2: InNF(TUnion ?t1 ?t2),
               Hsub: |- TUnion ?t1 ?t2 << _
               |- |- unite_pairs ?t (TUnion ?t1 ?t2) << TPair _ _] =>
              rewrite unite_pairs_t_union; try resolve_not_union;
              destruct (union_in_nf__components_in_nf _ _ Hnf2) as [Hnfb1 Hnfb2];
              destruct (union_nf_sub_r__components_sub_r _ _ _ Hsub Hnfb1 Hnfb2) as [Hsubb1 Hsubb2];
              constructor; [apply IHtb1 | apply IHtb2]; assumption
            | [Hnf1: InNF(?t), Hnf2: InNF(TUnion ?t1 ?t2),
               Hsub: |- TUnion ?t1 ?t2 << _
               |- |- unite_pairs (TUnion ?t1 ?t2) ?t << TPair _ _] =>
              rewrite unite_pairs_union_t;
              destruct (union_in_nf__components_in_nf _ _ Hnf2) as [Hnfb1 Hnfb2];
              destruct (union_nf_sub_r__components_sub_r _ _ _ Hsub Hnfb1 Hnfb2) as [Hsubb1 Hsubb2];
              constructor; [apply IHta1 | apply IHta2]; assumption
            end
          ].
Qed.

(* ================================================================= *)
(** *** About [MkNF] *)
(* ================================================================= *)

(* DEP: unite_pairs_of_nf__preserves_sub_r1 *)
Lemma sub_r__mk_nf_sub_r1 : forall (t t' : ty),
    |- t << t' ->
    |- MkNF(t) << t'.
Proof.
  intros t t' Hsub; induction Hsub;
    try solve [simpl; constructor; constructor].
  - (* Pair *)
    simpl.
    apply unite_pairs_of_nf__preserves_sub_r1;
      assumption || apply mk_nf__in_nf.
  - (* Union *)
    simpl. constructor; assumption.
  - (* UnionR1 *)
    apply SR_UnionR1; assumption.
  - (* UnionR2 *)
    apply SR_UnionR2; assumption.
  - (* NF *)
    assumption.
Qed.

(* DEP: unite_pairs_of_nf__preserves_sub_r1, mk_nf__in_nf *)
Lemma mk_nf__sub_r1 : forall (t : ty),
    |- MkNF(t) << t.
Proof.
  intros t.
  apply sub_r__mk_nf_sub_r1.
  apply sub_r__rflxv.
Qed.

Lemma mk_nf__sub_r2 : forall (t : ty),
    |- t << MkNF(t).
Proof.
  intros t.
  apply SR_NormalForm.
  apply sub_r__rflxv.
Qed.

(* ================================================================= *)
(** *** Related to Transitivity *)
(* ================================================================= *)

(* DEP: sub_r__mk_nf_sub_r1, union_nf_sub_r__components_sub_r *)
Lemma union_sub_r__components_sub_r : forall (t1 t2 t' : ty),
    |- TUnion t1 t2 << t' ->
    |- t1 << t' /\ |- t2 << t'.
Proof.
  intros t1 t2 t' Hsub.
  pose proof (sub_r__mk_nf_sub_r1 _ _ Hsub).
  simpl in H.
  assert (Hsubnf: |- MkNF(t1) << t' /\ |- MkNF(t2) << t').
  { apply union_nf_sub_r__components_sub_r;
      assumption || apply mk_nf__in_nf. }
  split; apply SR_NormalForm; tauto.
Qed.

(* DEP: sub_r_value_types__equal, union_in_nf__components_in_nf,
        mk_nf_nf__equal, mk_nf__in_nf *)
Lemma sub_r_nf__transitive : forall (t1 t2 t3 : ty),
    |- t1 << t2 ->
    InNF(t1) -> InNF(t2) ->
    |- t2 << t3 ->
    |- t1 << t3.
Proof.
  intros t1 t2 t3 Hsub1. generalize dependent t3.
  induction Hsub1; intros t3 Hnf1 Hnf2 Hsub2;
    try solve [
          assumption
        | inversion Hnf2; subst;
          match goal with [H: value_type _ |- _] => inversion H end
        | remember treal as t2 eqn:Heq2; induction Hsub2;
          inversion Heq2; subst; try solve [constructor | auto]
        | remember tnum as t2 eqn:Heq2; induction Hsub2;
          inversion Heq2; subst; try solve [constructor | auto]
        ].
  - (* Pair *)
    inversion Hnf1; subst. inversion Hnf2; subst.
    inversion H; inversion H0; subst.
    remember (TPair t1' t2') as tx eqn:Heqx; induction Hsub2;
      inversion Heqx; subst.
    + (* Pair *)
      constructor; [apply IHHsub1_1 | apply IHHsub1_2];
        try assumption || constructor; assumption.
    + (* UnionR1 *)
      apply SR_UnionR1; auto.
    + (* UnionR2 *)
      apply SR_UnionR2; auto.
    + (* NF *)
      apply IHHsub2.
      apply mk_nf_nf__equal; assumption. apply mk_nf__in_nf.
      rewrite mk_nf_nf__equal; assumption.
  - (* UnionL *)
    destruct (union_in_nf__components_in_nf _ _ Hnf1) as [Hnfa1 Hnfa2].
    constructor; [apply IHHsub1_1 | apply IHHsub1_2]; assumption.
  - (* UnionR1 *)
    destruct (union_in_nf__components_in_nf _ _ Hnf2) as [Hnfa1 Hnfa2].
    apply IHHsub1; try assumption.
    pose proof (union_nf_sub_r__components_sub_r _ _ _ Hsub2 Hnfa1 Hnfa2); tauto.
  - (* UnionR2 *)
    destruct (union_in_nf__components_in_nf _ _ Hnf2) as [Hnfa1 Hnfa2].
    apply IHHsub1; try assumption.
    pose proof (union_nf_sub_r__components_sub_r _ _ _ Hsub2 Hnfa1 Hnfa2); tauto.
  - (* NF *)
    rewrite mk_nf_nf__equal in IHHsub1; try assumption.
    apply IHHsub1; assumption.
Qed.

(* ################################################################# *)
(** ** Properties related to matching *)
(* ################################################################# *)

(* ================================================================= *)
(** *** Correctness of Subtyping with respect to Matching *)
(* ================================================================= *)

Theorem match_ty__sub_r_sound : forall (v t : ty),
    |- v <$ t ->
    |- v << t.
Proof.
  intros v t H; induction H; try solve [constructor].
  (* Pair *)   constructor; assumption.
  (* Union1 *) apply SR_UnionR1; assumption.
  (* Union2 *) apply SR_UnionR2; assumption.
Qed.

(* ================================================================= *)
(** ** Matching value Type is Complete for Subtyping *)
(* ================================================================= *)

(* DEP: match_valty__rflxv, mk_nf_valty__equal *)
Theorem match_valty__sub_r_complete : forall (v t : ty),
    |- v << t ->
    value_type v ->
    |- v <$ t.
Proof.
  intros v t H; induction H; subst; intros Hval;
    try solve [constructor | inversion Hval].
  - (* Pair *)
    inversion Hval; subst.
    constructor; tauto.
  - (* UnionR1 *)
    apply MT_Union1; tauto.
  - (* UnionR2 *)
    apply MT_Union2; tauto.
  - (* NF *)
    rewrite (mk_nf_atomty__equal _ (valty_atomty _ Hval)) in *.
    tauto.
Qed.

(* ################################################################# *)
(** ** Properties related to Normal Form *)
(* ################################################################# *)

(** If types are subtypes, their normal forms are also subtypes. *)
(* DEP: unite_pairs_of_nf__preserves_sub_r,
        mk_nf__in_nf, mk_nf__idempotent *)
Lemma sub_r__mk_nf_sub_r : forall (t t' : ty),
    |- t << t' ->
    |- MkNF(t) << MkNF(t').
Proof.
  intros t t' Hsub; induction Hsub;
    try solve [simpl; do 4 constructor].
  - (* Pair *)
    simpl.
    apply unite_pairs_of_nf__preserves_sub_r;
      assumption || apply mk_nf__in_nf.
  - (* Union *)
    simpl. constructor; assumption.
  - (* UnionR1 *)
    apply SR_UnionR1; assumption.
  - (* UnionR2 *)
    apply SR_UnionR2; assumption.
  - (* NF *)
    rewrite <- mk_nf__idempotent. assumption.
Qed.

(* DEP: mk_nf__in_nf *)
Lemma mk_nf_sub_r__sub_r : forall (t t' : ty),
    |- MkNF(t) << MkNF(t') ->
    |- t << t'.
Proof.
  intros t t' Hsub.
  apply SR_NormalForm.
  apply sub_r_nf__transitive with (MkNF(t')); try (apply mk_nf__in_nf).
  assumption. apply  mk_nf__sub_r1.
Qed.
(*
(* DEP: match_ty__sub_r_sound, match_valty__rflxv *)
Theorem nf_sem_sub__sub_r : forall (t : ty),
    InNF(t) ->
    forall (t' : ty),
      ||- [t] <= [t'] ->
      |- t << t'.
Proof.
  intros t Hnf; induction Hnf; intros t' Hval;
    unfold sem_sub.
  - (* Value *)
    apply match_ty__sub_r_sound. apply Hval.
    assumption. apply match_valty__rflxv. assumption.
  - (* Union *)
    constructor; [apply IHHnf1 | apply IHHnf2]; intros v Hv Hsub;
      try assumption; apply Hval; try assumption.
    apply MT_Union1; assumption.
    apply MT_Union2; assumption.
Qed.
*)

(* ################################################################# *)
(** ** Properties related to Declarative Subtyping *)
(* ################################################################# *)

(* ================================================================= *)
(** *** Reflexivity *)
(* ================================================================= *)

(* DEP: sub_r__rflxv *)
Lemma sub_r__reflexive : forall (t : ty),
    |- t << t.
Proof.
  apply sub_r__rflxv.
Qed.

(* ================================================================= *)
(** *** Transitivity *)
(* ================================================================= *)

(* DEP: sub_r__mk_nf_sub_r, sub_r_nf__transitive,
        mk_nf__in_nf, union_sub_r__components_sub_r *)
Lemma sub_r__transitive : forall (t1 t2 t3 : ty),
    |- t1 << t2 ->
    |- t2 << t3 ->
    |- t1 << t3.
Proof.
  intros t1 t2 t3 Hsub1. generalize dependent t3.
  induction Hsub1; intros t3 Hsub2;
    try (apply sub_r__mk_nf_sub_r1 in Hsub2; simpl in Hsub2;
         destruct (union_sub_r__components_sub_r _ _ _ Hsub2) as [Hsub21 Hsub22]);
    try (destruct (union_sub_r__components_sub_r _ _ _ Hsub21));
    try auto;
    try solve [
          remember treal as t2 eqn:Heq2; induction Hsub2;
          inversion Heq2; subst; try solve [constructor | auto]
        | remember tnum as t2 eqn:Heq2; induction Hsub2;
          inversion Heq2; subst; try solve [constructor | auto]
        ].
  (* Pair *)
  remember (TPair t1' t2') as tm eqn:Heq.
  induction Hsub2; try solve [inversion Heq].
  - (* Pair *)
    inversion Heq; subst.
    constructor; auto.
  - (* UnionR1 *)
    apply SR_UnionR1; tauto.
  - (* UnionR2 *)
    apply SR_UnionR2; tauto.
  - (* NF *)
    inversion Heq; subst. clear H.
    assert (Hsub1: |- TPair t1 t2 << TPair t1' t2') by (constructor; assumption).
    pose proof (sub_r__mk_nf_sub_r _ _ Hsub1) as Hsub1nf.
    apply SR_NormalForm.
    apply sub_r_nf__transitive with (MkNF( TPair t1' t2'));
      assumption || apply mk_nf__in_nf.
Qed.

(* ================================================================= *)
(** *** Distributivity *)
(* ================================================================= *)

(* ----------------------------------------------------------------- *)
(** **** Aux *)
(* ----------------------------------------------------------------- *)

(* DEP: unite_pairs_t_union, unite_pairs_union_t,
        sub_r__reflexive, sub_r__transitive *)
Lemma unite_pairs__distr21 : forall (t1 t21 t22 : ty),
    InNF(t1) ->
    |- unite_pairs t1 (TUnion t21 t22) <<
       TUnion (unite_pairs t1 t21) (unite_pairs t1 t22).
Proof.
  intros t1 t21 t22 Hnf1.
  generalize dependent t22. generalize dependent t21.
  induction Hnf1; intros t21 t22.
  - (* Value *)
    rewrite unite_pairs_t_union; try resolve_not_union.
    apply sub_r__reflexive. subst; inversion H.
  - (* Union *)
    repeat rewrite unite_pairs_union_t.
    constructor.
    + apply sub_r__transitive with (TUnion (unite_pairs t1 t21) (unite_pairs t1 t22)).
      apply IHHnf1_1. constructor.
      apply SR_UnionR1; apply SR_UnionR1; apply sub_r__reflexive.
      apply SR_UnionR2; apply SR_UnionR1; apply sub_r__reflexive.
    + apply sub_r__transitive with (TUnion (unite_pairs t2 t21) (unite_pairs t2 t22)).
      apply IHHnf1_2. constructor.
      apply SR_UnionR1; apply SR_UnionR2; apply sub_r__reflexive.
      apply SR_UnionR2; apply SR_UnionR2; apply sub_r__reflexive.
Qed.

(* ----------------------------------------------------------------- *)
(** **** Main Properties *)
(* ----------------------------------------------------------------- *)

(* DEP: unite_pairs_union_t, sub_r__reflexive *)
Lemma mk_nf__distr11 : forall (t11 t12 t2 : ty),
    |- MkNF(TPair (TUnion t11 t12) t2) << MkNF(TUnion (TPair t11 t2) (TPair t12 t2)).
Proof.
  intros t11 t12 t2.
  change (|- MkNF( TPair (TUnion t11 t12) t2) << TUnion (MkNF(TPair t11 t2)) (MkNF(TPair t12 t2))).
  change (|- unite_pairs (MkNF(TUnion t11 t12)) (MkNF(t2)) <<
             TUnion (MkNF(TPair t11 t2)) (MkNF(TPair t12 t2))).
  change (|- unite_pairs (TUnion (MkNF(t11)) (MkNF(t12))) (MkNF(t2)) <<
             TUnion (MkNF(TPair t11 t2)) (MkNF(TPair t12 t2))).
  rewrite unite_pairs_union_t.
  apply sub_r__reflexive.
Qed.

(* DEP: unite_pairs__distr21, mk_nf__in_nf *)
Lemma mk_nf__distr21 : forall (t1 t21 t22 : ty),
    |- MkNF(TPair t1 (TUnion t21 t22)) << MkNF(TUnion (TPair t1 t21) (TPair t1 t22)).
Proof.
  intros t1 t21 t22.
  change (|- MkNF(TPair t1 (TUnion t21 t22)) << TUnion (MkNF(TPair t1 t21)) (MkNF(TPair t1 t22))).
  change (|- unite_pairs (MkNF(t1)) (TUnion (MkNF(t21)) (MkNF(t22))) <<
             TUnion (MkNF(TPair t1 t21)) (MkNF(TPair t1 t22))).
  change (|- unite_pairs (MkNF(t1)) (TUnion (MkNF(t21)) (MkNF(t22))) <<
                               TUnion (unite_pairs (MkNF(t1)) (MkNF(t21))) (unite_pairs (MkNF(t1)) (MkNF(t22)))).
  apply unite_pairs__distr21.
  apply mk_nf__in_nf.
Qed.

(* ################################################################# *)
(** ** Examples *)
(* ################################################################# *)

Lemma not__real_sub_r_int :
  ~ (|- treal << tint).
Proof.
  remember treal as t1 eqn:Heq1. remember tint as t2 eqn:Heq2.
  intros Hcontra; induction Hcontra;
    try solve [inversion Heq1 | inversion Heq2].
  subst. tauto.
Qed.

Lemma not__real_sub_r_flt :
  ~ (|- treal << tflt).
Proof.
  remember treal as t1 eqn:Heq1. remember tflt as t2 eqn:Heq2.
  intros Hcontra; induction Hcontra;
    try solve [inversion Heq1 | inversion Heq2].
  subst. tauto.
Qed.

Lemma not__real_sub_r_u_int_flt :
  ~ (|- treal << TUnion tint tflt).
Proof.
  remember treal as t1 eqn:Heq1. remember (TUnion tint tflt) as t2 eqn:Heq2.
  intros Hcontra; induction Hcontra;
    try solve [inversion Heq1 | inversion Heq2].
  - inversion Heq1; inversion Heq2; subst.
    apply not__real_sub_r_int; tauto.
  - inversion Heq1; inversion Heq2; subst.
    apply not__real_sub_r_flt; tauto.
  - subst; tauto.
Qed.

(* ################################################################# *)
(** ** Decidability *)
(* ################################################################# *)

(* ----------------------------------------------------------------- *)
(** **** Aux *)
(* ----------------------------------------------------------------- *)

Lemma not__aname_sub_r_cname : forall (a : aname) (c : cname),
  ~ (|- TAName a << TCName c).
Proof.
  intros a c.
  remember (TAName a) as t1 eqn:Heq1. remember (TCName c) as t2 eqn:Heq2.
  intros Hcontra; induction Hcontra;
    try solve [inversion Heq1 | inversion Heq2].
  subst. tauto.
Qed.

Lemma not__aname_sub_r_pair : forall (a : aname) (t1 t2 : ty),
  ~ (|- TAName a << TPair t1 t2).
Proof.
  intros a t1 t2.
  remember (TAName a) as t eqn:Heq1. remember (TPair t1 t2) as t' eqn:Heq2.
  intros Hcontra; induction Hcontra;
    try solve [inversion Heq1 | inversion Heq2].
  subst. tauto.
Qed.

(*
Lemma aname_sub_r_union__aname_sub_r_component : forall (a : aname) (t1 t2 : ty),
    |- TAName a << TUnion t1 t2 ->
    |- TAName a << t1 \/ |- TAName a << t2.
Proof.
  intros a t1 t2.
  remember (TAName a) as t eqn:Heq1. remember (TUnion t1 t2) as t' eqn:Heq2.
  intros Hsub; induction Hsub;
    try solve [inversion Heq1 | inversion Heq2].
  - (* UnionR1 *)
    inversion Heq2; subst; tauto.
  - (* UnionR2 *)
    inversion Heq2; subst; tauto.
  - (* NF *)
    subst. simpl in IHHsub. tauto.
Qed.
*)

(* DEP: mk_nf_nf__equal, atomty_in_nf *)
Lemma atom_sub_r_union__atom_sub_r_component : forall (t t1 t2 : ty),
    atom_type t ->
    |- t << TUnion t1 t2 ->
    |- t << t1 \/ |- t << t2.
Proof.
  intros t t1 t2 Hat.
  remember (TUnion t1 t2) as t' eqn:Heq2.
  intros Hsub; induction Hsub;
    try solve [inversion Heq1 | inversion Heq2].
  - (* UnionL *)
    inversion Hat.
  - (* UnionR1 *)
    inversion Heq2; subst; tauto.
  - (* UnionR2 *)
    inversion Heq2; subst; tauto.
  - (* NF *)
    rewrite mk_nf_nf__equal in IHHsub.
    apply IHHsub; try assumption.
    apply atomty_in_nf; assumption.
Qed.

(* DEP: mk_nf_nf__equal *)
Lemma not__atom_pair_sub_r_cname : forall (c : cname) (t1 t2 : ty),
  atom_type t1 -> atom_type t2 ->
  ~ (|- TPair t1 t2 << TCName c).
Proof.
  intros c t1 t2 Hat1 Hat2.
  remember (TCName c) as t eqn:Heq1. remember (TPair t1 t2) as t' eqn:Heq2.
  intros Hcontra; induction Hcontra;
    try solve [inversion Heq1 | inversion Heq2].
  (* MkNF *)
  subst. apply IHHcontra. reflexivity.
  apply mk_nf_nf__equal. constructor. constructor; assumption.
Qed.

(* DEP: mk_nf_nf__equal *)
Lemma not__atom_pair_sub_r_aname : forall (a : aname) (t1 t2 : ty),
  atom_type t1 -> atom_type t2 ->
  ~ (|- TPair t1 t2 << TAName a).
Proof.
  intros a t1 t2 Hat1 Hat2.
  remember (TAName a) as t eqn:Heq1. remember (TPair t1 t2) as t' eqn:Heq2.
  intros Hcontra; induction Hcontra;
    try solve [inversion Heq1 | inversion Heq2].
  (* MkNF *)
  subst. apply IHHcontra. reflexivity.
  apply mk_nf_nf__equal. constructor. constructor; assumption.
Qed.

(* DEP: mk_nf_nf__equal *)
Lemma atom_pair_sub_r_pair__sub_r_components : forall (ta1 ta2 t1 t2 : ty),
    atom_type ta1 -> atom_type ta2 ->
    |- TPair ta1 ta2 << TPair t1 t2 ->
    |- ta1 << t1 /\ |- ta2 << t2.
Proof.
  intros ta1 ta2 t1 t2 Hta1 Hta2.
  remember (TPair ta1 ta2) as t eqn:Heq1. remember (TPair t1 t2) as t' eqn:Heq2.
  intros Hsub; induction Hsub;
    try solve [inversion Heq1 | inversion Heq2].
  - (* Pair *)
    inversion Heq1; inversion Heq2; subst; tauto.
  - (* NF *)
    subst. apply IHHsub; try reflexivity.
    apply mk_nf_nf__equal; repeat constructor; assumption.
Qed.

(* DEP: match_ty__dcdbl, match_ty__sub_r_sound, match_valty__sub_r_complete,
        not__aname_sub_r_cname, not__aname_sub_r_pair,
        atom_pair_sub_r_pair__sub_r_components,
        atom_sub_r_union__atom_sub_r_component *)
Lemma atom_sub_r__decidable : forall (t1 t2 : ty),
    atom_type t1 ->
    Decidable.decidable (|- t1 << t2).
Proof.
  intros t1 t2 Hat1. generalize dependent t2.
  induction Hat1.
  - (* CName *)
    intros t2. destruct (match_ty__dcdbl (TCName n) t2) as [Hm | Hm].
    + left. apply match_ty__sub_r_sound. assumption.
    + right; intros Hcontra.
      assert (Hcontra': |- (TCName n) <$ t2)
        by (apply match_valty__sub_r_complete; assumption || constructor).
      contradiction.
  - (* AName *)
    intros t2; induction t2.
    + (* CName *)
      right. apply not__aname_sub_r_cname.
    + (* AName *)
      destruct n; destruct a;
        try solve [left; apply sub_r__rflxv || constructor].
      right. intros Hcontra.
      remember (TAName NNum) as t1 eqn:Heq1. remember (TAName NReal) as t2 eqn:Heq2.
      induction Hcontra;
        try solve [inversion Heq1 | inversion Heq2].
      inversion Heq1; inversion Heq2; subst.
      inversion H1. subst. tauto.
    + (* Pair *)
      right. apply not__aname_sub_r_pair.
    + (* Union *)
      destruct IHt2_1 as [IH1 | IH1];
        destruct IHt2_2 as [IH2 | IH2];
        try solve [
              left; apply SR_UnionR1; assumption
            | left; apply SR_UnionR2; assumption ].
      right; intros Hcontra.
      apply atom_sub_r_union__atom_sub_r_component in Hcontra.
      tauto. constructor.
  - (* Pair *)
    intros t'. induction t'.
    + (* CName *)
      right; apply not__atom_pair_sub_r_cname; assumption.
    + (* AName *)
      right; apply not__atom_pair_sub_r_aname; assumption.
    + (* Pair *)
      destruct (IHHat1_1 t'1) as [IH1 | IH1];
        destruct (IHHat1_2 t'2) as [IH2 | IH2];
        solve [
            left; constructor; assumption
          | right; intros Hcontra;
            apply atom_pair_sub_r_pair__sub_r_components in Hcontra;
            try assumption;
            destruct Hcontra as [Hsub1 Hsub2]; contradiction ].
    + (* Union *)
      destruct IHt'1 as [IH1 | IH1];
        destruct IHt'2 as [IH2 | IH2];
        try solve [
              left; apply SR_UnionR1; assumption
            | left; apply SR_UnionR2; assumption ].
      right; intros Hcontra.
      apply atom_sub_r_union__atom_sub_r_component in Hcontra.
      tauto. constructor; assumption.
Qed.

(* ----------------------------------------------------------------- *)
(** **** Main Properties *)
(* ----------------------------------------------------------------- *)

(* DEP: atom_sub_r__decidable, union_sub_r__components_sub_r *)
Lemma nf_sub_r__decidable : forall (t1 t2 : ty),
    InNF(t1) ->
    Decidable.decidable (|- t1 << t2).
Proof.
  intros t1 t2 Hnf1. generalize dependent t2.
  induction Hnf1.
  - (* Atom *)
    intros t2. destruct (atom_sub_r__decidable ta t2 H) as [Hm | Hm].
    + left; assumption.
    + right; assumption.
  - (* Union *)
    intros t'.
    destruct (IHHnf1_1 t') as [IH1 | IH1];
      destruct (IHHnf1_2 t') as [IH2 | IH2];
      try solve [
            right; intros Hcontra;
            destruct (union_sub_r__components_sub_r _ _ _ Hcontra) as [Hsub1 Hsub2];
            contradiction ].
    left; constructor; assumption.
Qed.

author: julbinb


text:
Require Import Coq.Arith.Arith.
Require Import Coq.Strings.String.
Require Import Maps.
Require Import Coq.Logic.FunctionalExtensionality.
Import Setoid.

Module MSkip.

Definition state := total_map nat.

Inductive com : Type :=
| CSkip : com
.

Inductive ceval : com -> state -> state -> Prop :=
| E_Skip : forall s:state, ceval CSkip s s
.

Theorem ceval_deterministic : forall (c:com) (src:state) (dst1:state) (dst2:state),
ceval c src dst1 -> ceval c src dst2 -> dst1 = dst2.
intros c src dst1 dst2.
intros h1 h2.
inversion h1. subst s. subst dst1.
subst c.
inversion h2. subst s. subst dst2.
reflexivity.
Qed.

Theorem nothing: forall (c:com) (src dst:state),
ceval c src dst -> src = dst.
intros c src dst.
intro h. inversion h. reflexivity.
Qed.

End MSkip.

Module MAssignment.

Definition state := partial_map nat.

Inductive com : Type :=
| CSkip : com
| CAss : string -> nat -> com
.

Inductive ceval : com -> state -> state -> Prop :=
| E_Skip : forall s:state, ceval CSkip s s
| E_Ass : forall (s:state) (id:string) (n:nat), ceval (CAss id n) s (update s id n)
.

Theorem alln : forall (n:nat) (src dst:state), exists (c:com), ceval c src dst -> exists id:string, dst id = Some n.
intros n src dst.
exists (CAss "A" n).
intro h.
exists "A"%string.
inversion h. subst n0. subst id. subst s.
unfold update.
unfold t_update.
rewrite beq_string_refl.
reflexivity.
Qed.

Theorem state_different_single_variable : forall (src dst:state) (c:com),
src=empty /\ ceval c src dst /\ src <> dst ->
exists (id:string) (n:nat), dst id = Some n /\
  forall (id':string) (n':nat), dst id' = Some n' -> n=n' /\ id=id'.
Proof.
intros src dst c.
intros [empty [heval hneq]].
inversion heval.
subst c. subst s. subst src. contradiction.
subst s. exists id. exists n.
split.
unfold update. unfold t_update. rewrite beq_string_refl. reflexivity.
intros id' n'.
intro update'.
unfold update in update'.
unfold t_update in update'.
subst c.

unfold beq_string in update'.
destruct (string_dec id id').
subst id'.
inversion update'.
subst n'.
split;reflexivity.

subst src. inversion update'.

Qed.

End MAssignment.

Module MSkipAndSeq.

Definition state := partial_map nat.

Inductive com : Type :=
| CSkip : com
| CSeq : com -> com -> com
.

Inductive ceval : com -> state -> state -> Prop :=
| E_Skip : forall s:state, ceval CSkip s s
| E_Seq : forall (src tmp dst:state) (c1 c2:com), ceval c1 src tmp -> ceval c2 tmp dst -> ceval (CSeq c1 c2) src dst
.

Theorem nothing : forall (src dst:state) (c:com), ceval c src dst -> src = dst.
Proof.
intros src dst c.
generalize src dst.
clear src dst.
induction c.
intros src dst heval. inversion heval. reflexivity.
intros src dst heval.
inversion heval.
subst dst0 src0 c3 c0.
rewrite <- (IHc2 tmp dst).
rewrite <- (IHc1 src tmp).
reflexivity. assumption. assumption.
Qed.

Theorem nothing2 : forall (s:state) (c:com), ceval c s s.
Proof.
intros s c. generalize s. clear s. induction c.
intros;constructor.
intro s.
apply (E_Seq s s s). apply IHc1. apply IHc2.
Qed.

Theorem something_impossible : forall (src dst:state) (c:com), not (ceval c src dst /\ src <> dst).
intros src dst c.
intros [heval hneq].
apply hneq.
rewrite (nothing src dst c). reflexivity. assumption.
Qed.

Fixpoint contains_skip (c:com) : Prop :=
match c with
| CSkip => True
| CSeq c1 c2 => (contains_skip c1) \/ (contains_skip c2)
end.

Theorem must_skip : forall (src dst:state) (c:com), ceval c src dst -> contains_skip c.
intros src dst c.
generalize dependent dst.
generalize dependent src.
induction c.
simpl. trivial.
intros src dst heval.
simpl.
inversion heval.
subst dst0 src0 c3 c0.
right. apply (IHc2 tmp dst). assumption.
Qed.

Fixpoint depth (c:com) : nat :=
match c with
| CSkip => 0
| CSeq c1 c2 => S (max (depth c1) (depth c2))
end.

Theorem any_depth : forall (s:state) (n:nat), exists c:com, depth c = n /\ ceval c s s.
intros s n.
generalize dependent s.
induction n.
intro s. exists CSkip. simpl. split. reflexivity. constructor.
intro s.
specialize (IHn s).
inversion_clear IHn as [c' [hdepth heval]].
exists (CSeq c' c').
simpl.
rewrite Nat.max_id.
rewrite hdepth. split. reflexivity. apply (E_Seq s s s). assumption. assumption.
Qed.

Theorem depth_0_Skip : forall (s:state) (c:com), depth c = 0 -> ceval c s s -> c = CSkip.
intros s c hdepth heval.
destruct c. reflexivity.
simpl in hdepth. inversion hdepth.
Qed.

Fixpoint count_skip (c:com) : nat :=
match c with
| CSkip => 1
| CSeq c1 c2 => (count_skip c1) + (count_skip c2)
end.

Search "even".

Theorem nm0 : forall (n m:nat), n+m=0->n=0/\m=0.
intro n. induction n.
destruct m. simpl. intro;split;reflexivity.
simpl. intro h;inversion h.
intro m. simpl. intro h. inversion h.
Qed.

Theorem nm1 : forall (n m :nat), n+m=1->n=1\/m=1.
intro n. induction n.
simpl. intros m h. right. assumption.
simpl.
intros m h. inversion h. apply nm0 in H0.
inversion_clear H0 as [n0 m0].
subst m. subst n.
simpl. left. reflexivity.
Qed.

Theorem count_skip_nonzero : forall (src dst:state) (c:com), ceval c src dst -> count_skip c <> 0.
intros src dst.
intro c.
generalize dependent dst.
generalize dependent src.
induction c.
simpl. intros. intro impossible. inversion impossible.
intros src dst.
intro heval.
intro hcs.
inversion heval.
subst dst0. subst src0. subst c3. subst c0.
simpl in hcs.
apply nm0 in hcs. inversion_clear hcs as [h1 h2].
apply (IHc2 tmp dst). assumption. assumption.
Qed.

Fixpoint count_all (c:com) : nat :=
match c with
| CSkip => 1
| CSeq c1 c2 => 1 + count_all(c1) + count_all(c2)
end.

Theorem no2 : forall (c:com), count_all c <> 2.
Proof.
intros c.
induction c.
simpl. intros. trivial.
intros.
destruct c1;destruct c2.
simpl. auto.
simpl. intro h. inversion h.
simpl. intro h. inversion h.

simpl in IHc1.

apply nm0 in H0. inversion H0. inversion H1.

simpl. intro h.
inversion h. clear h.
apply nm0 in H0. inversion_clear H0.
inversion H1.
Qed.

Fixpoint count_seq (c:com) : nat :=
match c with
| CSkip => 0
| CSeq x y => 1 + (count_seq x) + (count_seq y)
end.

Theorem nGt0_npnGt1 : forall n:nat, n>0 -> n+n>1.
intros n h.
destruct h. auto. simpl. rewrite plus_comm. simpl.
clear h.
induction m. auto. simpl. rewrite plus_comm. simpl.
apply (gt_trans _ (S(S(m+m))) _).
auto. assumption.
Qed.

Theorem nmGtOnpmGt1 : forall (n m:nat), n>0 -> m>0 -> n+m>1.
unfold gt. unfold lt.
intros n m hn hm.
induction hn. simpl.
Search ( _ <= _ -> _ <= _).
apply le_n_S. assumption.
rename m0 into n. destruct hm. simpl. apply (le_trans _ (n+1) _). assumption. auto.
apply (le_trans _ (n + S m) _). assumption.
simpl. rewrite plus_comm at 2. simpl. rewrite plus_comm at 1. simpl. auto.
Qed.

Theorem more_skip_helper : forall (n m o p : nat), n > S o -> m > S p -> n + m > S(S o + S p).
unfold gt. unfold lt.
intros n m o p.
intros hon.
induction hon. simpl. intros.
Search (_ <= _ -> S _ <= S _).
apply le_n_S. apply le_n_S.
rewrite plus_n_Sm.
Search ( _ <= _ -> _ + _ <= _ + _ ).
apply plus_le_compat_l. assumption.
simpl. intros.
rename m0 into q.
simpl in IHhon.
apply (le_trans _ (q+m) _).
apply IHhon. assumption.
rewrite plus_n_Sm.
apply plus_le_compat_l. auto.
Qed.

Theorem more_skip : forall (c:com), count_skip c > count_seq c.
induction c.
simpl. auto.
simpl.
destruct c1;destruct c2.
simpl. auto.
simpl. simpl in IHc1. simpl in IHc2.
rename c2_1 into a. rename c2_2 into b.
Search (_ > _ -> S _ > S _). apply gt_n_S. assumption.
simpl. simpl in IHc1. simpl in IHc2.
rewrite plus_comm at 1. simpl. apply gt_n_S.
Search ( _ + 0).
rewrite <- plus_n_O. assumption.
rename c1_1 into a. rename c1_2 into b. rename c2_1 into c. rename c2_2 into d.
simpl in IHc1. simpl in IHc2.
simpl.
apply more_skip_helper. assumption. assumption.
Qed.

Theorem any_skip : forall (n:nat), n<>0 -> exists (c:com), count_skip c = n.
destruct n. intro h. contradiction.
intro h. clear h.
induction n. exists CSkip. simpl. reflexivity.
inversion IHn.
exists (CSeq CSkip x ).
simpl. rewrite H. reflexivity.
Qed.

Theorem any_seq : forall (n:nat), exists (c:com), count_seq c = n.
induction n. exists CSkip. simpl. reflexivity.
inversion IHn. exists (CSeq CSkip x). simpl. rewrite H. reflexivity.
Qed.

Theorem all1orgt2_helper : forall n m o : nat, o <= n -> o <= m -> o <= n + m.
intros n m o hon .
induction hon.
intro.
apply (le_trans _ m _). assumption.
rewrite plus_comm.
rewrite plus_n_O at 1.
apply plus_le_compat_l.
apply le_0_n.
intro hom. destruct hom. simpl. rename m0 into n.
apply (le_trans _ (n+o) _). apply IHhon. auto. auto.
rename m0 into n.
apply (le_trans _ (n + S m) _).
apply IHhon. apply (le_trans _ m _). assumption. auto.
simpl. rewrite plus_comm at 2. simpl. rewrite plus_comm. simpl. auto.
Qed.

Theorem all1orgt2 : forall (c:com), count_all c = 1 \/ count_all c > 2.
unfold gt. unfold lt.
induction c. simpl. left. reflexivity.
right. inversion IHc1 ; inversion IHc2.
simpl. rewrite H. rewrite H0. simpl. auto.
simpl. rewrite H. apply (le_trans _ (count_all c2) _). assumption. simpl. auto.
simpl. rewrite H0. apply (le_trans _ (count_all c1) _). assumption.
rewrite plus_comm. simpl. auto.
simpl. apply (le_trans _ (count_all c1+count_all c2) _).
apply all1orgt2_helper. assumption. assumption.
auto.
Qed.

End MSkipAndSeq.

Module MSkipSeqAss.

Definition state := partial_map nat.

Inductive com : Type :=
| CSkip : com
| CAss : string -> nat -> com
| CSeq : com -> com -> com
.

Inductive ceval : com -> state -> state -> Prop :=
| E_Skip : forall s:state, ceval CSkip s s
| E_Ass : forall (s:state) (id:string) (n:nat), ceval (CAss id n) s (update s id n)
| E_Seq : forall (src tmp dst:state) (c1 c2:com), ceval c1 src tmp -> ceval c2 tmp dst -> ceval (CSeq c1 c2) src dst
.

Fixpoint count_skip (c:com) : nat :=
match c with
| CSkip => 1
| CAss _ _ => 0
| CSeq x y => (count_skip x) + (count_skip y)
end.

Theorem no_skip_ass : forall (c:com) (src dst:state),
ceval c src dst ->
count_skip c = 0 ->
exists (s:string) (n:nat), dst s = Some n.
Proof.
intros c src dst.
generalize dependent dst.
generalize dependent src.
induction c.
simpl. intros. inversion H0.
simpl. intros. inversion H. subst s0 n0 s. exists id, n.
unfold update. unfold t_update. rewrite beq_string_refl. reflexivity.
simpl. intros.
apply MSkipAndSeq.nm0 in H0. inversion_clear H0.
inversion H. subst c0 c3 src0 dst0.
specialize (IHc2 tmp dst H7 H2).
inversion IHc2. inversion H0.
rename x into id. rename x0 into n.
exists id. exists n.
assumption.
Qed.

Fixpoint count_seq (c:com) : nat :=
match c with
| CSkip => 0
| CAss _ _ => 0
| CSeq x y => (count_seq x)+(count_seq y)+1
end.

Theorem if_ass_then_unique : forall (c:com) (src dst:state) (s:string) (n:nat),
count_seq c = 0 ->
ceval c src dst ->
(forall s:string, src s = None) ->
dst s = Some n ->
(forall (s':string) (n':nat), dst s' = Some n' -> s=s' /\ n=n').
Proof.
intros c src dst.
generalize dependent dst.
generalize dependent src.
induction c as [ | id n | ].
{
  simpl.
  intros src dst id n oo heval hnone hidn id' n' hidn'.
  (* cleanup *) clear oo.
  inversion heval as [ src' skipeq srceq srcdsteq | | ].
  (* cleanup *) clear heval skipeq. subst dst. subst src'. clear hidn'.
  (* more cleanup *) apply False_ind. clear id' n'.
  rewrite (hnone id) in hidn.
  inversion hidn.
}
{
  simpl.
  intros src dst id' n' oo heval hnone hidn' id'' n'' hidn''.
  (* cleanup *) clear oo.
  inversion heval as [ | src' id''' n''' ideq neq sind | ].
  subst id''' n'''.
  subst src'.
  rewrite <- sind in hidn'.
  rewrite <- sind in hidn''.
  (* cleanup *) clear sind.
  unfold update in hidn', hidn''.
  unfold t_update in hidn', hidn''.
  unfold beq_string in hidn', hidn''.
  destruct (string_dec id id');destruct (string_dec id id'').
  - inversion hidn''. subst n''. inversion hidn'. subst n'. subst id''. subst id'. split;reflexivity.
  - rewrite (hnone id'') in hidn''. inversion hidn''.
  - rewrite (hnone id') in hidn'. inversion hidn'.
  - rewrite (hnone id') in hidn'. inversion hidn'.
}
{
  simpl.
  intros src dst id n cso heval hnone hidn id' n' hidn'.
  apply MSkipAndSeq.nm0 in cso. inversion cso as [l r]. inversion r.
}
Qed.

End MSkipSeqAss.

author: xavierdpt

repo: research

save_path: github-repos/coq/xavierdpt-research


text:
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Nnat.
Require Import ArithRing.
Require Export Ring Field.
Require Import Rdefinitions.
Require Import Rpow_def.
Require Import Raxioms.

Local Open Scope R_scope.

Lemma RTheory : ring_theory 0 1 Rplus Rmult Rminus Ropp (eq (A:=R)).
Proof.
constructor.
 intro; apply Rplus_0_l.
 exact Rplus_comm.
 symmetry ; apply Rplus_assoc.
 intro; apply Rmult_1_l.
 exact Rmult_comm.
 symmetry ; apply Rmult_assoc.
 intros m n p.
   rewrite Rmult_comm.
   rewrite (Rmult_comm n p).
   rewrite (Rmult_comm m p).
   apply Rmult_plus_distr_l.
 reflexivity.
 exact Rplus_opp_r.
Qed.

Lemma Rfield : field_theory 0 1 Rplus Rmult Rminus Ropp Rdiv Rinv (eq(A:=R)).
Proof.
constructor.
 exact RTheory.
 exact R1_neq_R0.
 reflexivity.
 exact Rinv_l.
Qed.

Lemma Rlt_n_Sn : forall x, x < x + 1.
Proof.
intro.
elim archimed with x; intros.
destruct H0.
 apply Rlt_trans with (IZR (up x)); trivial.
    replace (IZR (up x)) with (x + (IZR (up x) - x))%R.
  apply Rplus_lt_compat_l; trivial.
  unfold Rminus.
    rewrite (Rplus_comm (IZR (up x)) (- x)).
    rewrite <- Rplus_assoc.
    rewrite Rplus_opp_r.
    apply Rplus_0_l.
 elim H0.
   unfold Rminus.
   rewrite (Rplus_comm (IZR (up x)) (- x)).
   rewrite <- Rplus_assoc.
   rewrite Rplus_opp_r.
   rewrite Rplus_0_l; trivial.
Qed.

Notation Rset := (Eqsth R).
Notation Rext := (Eq_ext Rplus Rmult Ropp).

Lemma Rlt_0_2 : 0 < 2.
Proof.
apply Rlt_trans with (0 + 1).
 apply Rlt_n_Sn.
 rewrite Rplus_comm.
   apply Rplus_lt_compat_l.
    replace R1 with (0 + 1).
  apply Rlt_n_Sn.
  apply Rplus_0_l.
Qed.

Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0.
unfold Rgt.
induction x; simpl; intros.
 apply Rlt_trans with (1 + 0).
  rewrite Rplus_comm.
    apply Rlt_n_Sn.
  apply Rplus_lt_compat_l.
    rewrite <- (Rmul_0_l Rset Rext RTheory 2).
    rewrite Rmult_comm.
    apply Rmult_lt_compat_l.
   apply Rlt_0_2.
   trivial.
 rewrite <- (Rmul_0_l Rset Rext RTheory 2).
   rewrite Rmult_comm.
   apply Rmult_lt_compat_l.
  apply Rlt_0_2.
  trivial.
  replace 1 with (0 + 1).
  apply Rlt_n_Sn.
  apply Rplus_0_l.
Qed.

Lemma Rgen_phiPOS_not_0 :
  forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0.
red; intros.
specialize (Rgen_phiPOS x).
rewrite H; intro.
apply (Rlt_asym 0 0); trivial.
Qed.

Lemma Zeq_bool_complete : forall x y,
  InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x =
  InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y ->
  Zeq_bool x y = true.
Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0.

Lemma Rdef_pow_add : forall (x:R) (n m:nat), pow x  (n + m) = pow x n * pow x m.
Proof.
  intros x n; elim n; simpl; auto with real.
  intros n0 H' m; rewrite H'; auto with real.
Qed.

Lemma R_power_theory : power_theory 1%R Rmult (@eq R) N.to_nat pow.
Proof.
 constructor. destruct n. reflexivity.
 simpl. induction p.
 - rewrite Pos2Nat.inj_xI. simpl. now rewrite plus_0_r, Rdef_pow_add, IHp.
 - rewrite Pos2Nat.inj_xO. simpl. now rewrite plus_0_r, Rdef_pow_add, IHp.
 - simpl. rewrite Rmult_comm;apply Rmult_1_l.
Qed.

Ltac Rpow_tac t :=
  match isnatcst t with
  | false => constr:(InitialRing.NotConstant)
  | _ => constr:(N.of_nat t)
  end.

Ltac IZR_tac t :=
  match t with
  | R0 => constr:(0%Z)
  | R1 => constr:(1%Z)
  | IZR ?u =>
    match isZcst u with
    | true => u
    | _ => constr:(InitialRing.NotConstant)
    end
  | _ => constr:(InitialRing.NotConstant)
  end.

Add Field RField : Rfield
   (completeness Zeq_bool_complete, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]).

author: Priyanka-Mondal

repo: Coq

save_path: github-repos/coq/Priyanka-Mondal-Coq