text:
From Hammer Require Import Hammer.

Require Export BinNums.
Require Import BinPos RelationClasses Morphisms Setoid
Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties.
Require BinNatDef.

Local Open Scope N_scope.

Module N
<: NAxiomsSig
<: UsualOrderedTypeFull
<: UsualDecidableTypeFull
<: TotalOrder.

Include BinNatDef.N.

Set Inline Level 30.

Definition eq := @Logic.eq N.
Definition eq_equiv := @eq_equivalence N.

Definition lt x y := (x ?= y) = Lt.
Definition gt x y := (x ?= y) = Gt.
Definition le x y := (x ?= y) <> Gt.
Definition ge x y := (x ?= y) <> Lt.

Infix "<=" := le : N_scope.
Infix "<" := lt : N_scope.
Infix ">=" := ge : N_scope.
Infix ">" := gt : N_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : N_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : N_scope.
Notation "x < y < z" := (x < y /\ y < z) : N_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : N_scope.

Definition divide p q := exists r, q = r*p.
Notation "( p | q )" := (divide p q) (at level 0) : N_scope.

Definition Even n := exists m, n = 2*m.
Definition Odd n := exists m, n = 2*m+1.

Local Obligation Tactic := simpl_relation.
Program Definition succ_wd : Proper (eq==>eq) succ := _.
Program Definition pred_wd : Proper (eq==>eq) pred := _.
Program Definition add_wd : Proper (eq==>eq==>eq) add := _.
Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.

Definition eq_dec : forall n m : N, { n = m } + { n <> m }.
Proof. hammer_hook "BinNat" "BinNat.N.eq_dec".
decide equality.
apply Pos.eq_dec.
Defined.

Definition discr n : { p:positive | n = pos p } + { n = 0 }.
Proof. hammer_hook "BinNat" "BinNat.N.discr".
destruct n; auto.
left; exists p; auto.
Defined.

Definition binary_rect (P:N -> Type) (f0 : P 0)
(f2 : forall n, P n -> P (double n))
(fS2 : forall n, P n -> P (succ_double n)) (n : N) : P n :=
let P' p := P (pos p) in
let f2' p := f2 (pos p) in
let fS2' p := fS2 (pos p) in
match n with
| 0 => f0
| pos p => positive_rect P' fS2' f2' (fS2 0 f0) p
end.

Definition binary_rec (P:N -> Set) := binary_rect P.
Definition binary_ind (P:N -> Prop) := binary_rect P.

Definition peano_rect
(P : N -> Type) (f0 : P 0)
(f : forall n : N, P n -> P (succ n)) (n : N) : P n :=
let P' p := P (pos p) in
let f' p := f (pos p) in
match n with
| 0 => f0
| pos p => Pos.peano_rect P' (f 0 f0) f' p
end.

Theorem peano_rect_base P a f : peano_rect P a f 0 = a.
Proof. hammer_hook "BinNat" "BinNat.N.peano_rect_base".
reflexivity.
Qed.

Theorem peano_rect_succ P a f n :
peano_rect P a f (succ n) = f n (peano_rect P a f n).
Proof. hammer_hook "BinNat" "BinNat.N.peano_rect_succ".
destruct n; simpl.
trivial.
now rewrite Pos.peano_rect_succ.
Qed.

Definition peano_ind (P : N -> Prop) := peano_rect P.

Definition peano_rec (P : N -> Set) := peano_rect P.

Theorem peano_rec_base P a f : peano_rec P a f 0 = a.
Proof. hammer_hook "BinNat" "BinNat.N.peano_rec_base".
apply peano_rect_base.
Qed.

Theorem peano_rec_succ P a f n :
peano_rec P a f (succ n) = f n (peano_rec P a f n).
Proof. hammer_hook "BinNat" "BinNat.N.peano_rec_succ".
apply peano_rect_succ.
Qed.

Theorem bi_induction :
forall A : N -> Prop, Proper (Logic.eq==>iff) A ->
A 0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n.
Proof. hammer_hook "BinNat" "BinNat.N.bi_induction".
intros A A_wd A0 AS. apply peano_rect. assumption. intros; now apply -> AS.
Qed.

Definition recursion {A} : A -> (N -> A -> A) -> N -> A :=
peano_rect (fun _ => A).

Instance recursion_wd {A} (Aeq : relation A) :
Proper (Aeq==>(Logic.eq==>Aeq==>Aeq)==>Logic.eq==>Aeq) recursion.
Proof. hammer_hook "BinNat" "BinNat.N.recursion_wd".
intros a a' Ea f f' Ef x x' Ex. subst x'.
induction x using peano_ind.
trivial.
unfold recursion in *. rewrite 2 peano_rect_succ. now apply Ef.
Qed.

Theorem recursion_0 {A} (a:A) (f:N->A->A) : recursion a f 0 = a.
Proof. hammer_hook "BinNat" "BinNat.N.recursion_0".   reflexivity. Qed.

Theorem recursion_succ {A} (Aeq : relation A) (a : A) (f : N -> A -> A):
Aeq a a -> Proper (Logic.eq==>Aeq==>Aeq) f ->
forall n : N, Aeq (recursion a f (succ n)) (f n (recursion a f n)).
Proof. hammer_hook "BinNat" "BinNat.N.recursion_succ".
unfold recursion; intros a_wd f_wd n. induction n using peano_ind.
rewrite peano_rect_succ. now apply f_wd.
rewrite !peano_rect_succ in *. now apply f_wd.
Qed.

Lemma one_succ : 1 = succ 0.
Proof. hammer_hook "BinNat" "BinNat.N.one_succ".   reflexivity. Qed.

Lemma two_succ : 2 = succ 1.
Proof. hammer_hook "BinNat" "BinNat.N.two_succ".   reflexivity. Qed.

Definition pred_0 : pred 0 = 0.
Proof. hammer_hook "BinNat" "BinNat.N.pred_0".   reflexivity. Qed.

Lemma pos_pred_spec p : Pos.pred_N p = pred (pos p).
Proof. hammer_hook "BinNat" "BinNat.N.pos_pred_spec".
now destruct p.
Qed.

Lemma succ_pos_spec n : pos (succ_pos n) = succ n.
Proof. hammer_hook "BinNat" "BinNat.N.succ_pos_spec".
now destruct n.
Qed.

Lemma pos_pred_succ n : Pos.pred_N (succ_pos n) = n.
Proof. hammer_hook "BinNat" "BinNat.N.pos_pred_succ".
destruct n. trivial. apply Pos.pred_N_succ.
Qed.

Lemma succ_pos_pred p : succ (Pos.pred_N p) = pos p.
Proof. hammer_hook "BinNat" "BinNat.N.succ_pos_pred".
destruct p; simpl; trivial. f_equal. apply Pos.succ_pred_double.
Qed.

Theorem pred_succ n : pred (succ n) = n.
Proof. hammer_hook "BinNat" "BinNat.N.pred_succ".
destruct n; trivial. simpl. apply Pos.pred_N_succ.
Qed.

Theorem pred_sub n : pred n = sub n 1.
Proof. hammer_hook "BinNat" "BinNat.N.pred_sub".
now destruct n as [|[p|p|]].
Qed.

Theorem succ_0_discr n : succ n <> 0.
Proof. hammer_hook "BinNat" "BinNat.N.succ_0_discr".
now destruct n.
Qed.

Theorem add_0_l n : 0 + n = n.
Proof. hammer_hook "BinNat" "BinNat.N.add_0_l".
reflexivity.
Qed.

Theorem add_succ_l n m : succ n + m = succ (n + m).
Proof. hammer_hook "BinNat" "BinNat.N.add_succ_l".
destruct n, m; unfold succ, add; now rewrite ?Pos.add_1_l, ?Pos.add_succ_l.
Qed.

Theorem sub_0_r n : n - 0 = n.
Proof. hammer_hook "BinNat" "BinNat.N.sub_0_r".
now destruct n.
Qed.

Theorem sub_succ_r n m : n - succ m = pred (n - m).
Proof. hammer_hook "BinNat" "BinNat.N.sub_succ_r".
destruct n as [|p], m as [|q]; trivial.
now destruct p.
simpl. rewrite Pos.sub_mask_succ_r, Pos.sub_mask_carry_spec.
now destruct (Pos.sub_mask p q) as [|[r|r|]|].
Qed.

Theorem mul_0_l n : 0 * n = 0.
Proof. hammer_hook "BinNat" "BinNat.N.mul_0_l".
reflexivity.
Qed.

Theorem mul_succ_l n m : (succ n) * m = n * m + m.
Proof. hammer_hook "BinNat" "BinNat.N.mul_succ_l".
destruct n, m; simpl; trivial. f_equal. rewrite Pos.add_comm.
apply Pos.mul_succ_l.
Qed.

Lemma eqb_eq n m : eqb n m = true <-> n=m.
Proof. hammer_hook "BinNat" "BinNat.N.eqb_eq".
destruct n as [|n], m as [|m]; simpl; try easy'.
rewrite Pos.eqb_eq. split; intro H. now subst. now destr_eq H.
Qed.

Lemma ltb_lt n m : (n <? m) = true <-> n < m.
Proof. hammer_hook "BinNat" "BinNat.N.ltb_lt".
unfold ltb, lt. destruct compare; easy'.
Qed.

Lemma leb_le n m : (n <=? m) = true <-> n <= m.
Proof. hammer_hook "BinNat" "BinNat.N.leb_le".
unfold leb, le. destruct compare; easy'.
Qed.

Theorem compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
Proof. hammer_hook "BinNat" "BinNat.N.compare_eq_iff".
destruct n, m; simpl; rewrite ?Pos.compare_eq_iff; split; congruence.
Qed.

Theorem compare_lt_iff n m : (n ?= m) = Lt <-> n < m.
Proof. hammer_hook "BinNat" "BinNat.N.compare_lt_iff".
reflexivity.
Qed.

Theorem compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.
Proof. hammer_hook "BinNat" "BinNat.N.compare_le_iff".
reflexivity.
Qed.

Theorem compare_antisym n m : (m ?= n) = CompOpp (n ?= m).
Proof. hammer_hook "BinNat" "BinNat.N.compare_antisym".
destruct n, m; simpl; trivial. apply Pos.compare_antisym.
Qed.

Include BoolOrderFacts.

Theorem min_l n m : n <= m -> min n m = n.
Proof. hammer_hook "BinNat" "BinNat.N.min_l".
unfold min, le. case compare; trivial. now destruct 1.
Qed.

Theorem min_r n m : m <= n -> min n m = m.
Proof. hammer_hook "BinNat" "BinNat.N.min_r".
unfold min, le. rewrite compare_antisym.
case compare_spec; trivial. now destruct 2.
Qed.

Theorem max_l n m : m <= n -> max n m = n.
Proof. hammer_hook "BinNat" "BinNat.N.max_l".
unfold max, le. rewrite compare_antisym.
case compare_spec; auto. now destruct 2.
Qed.

Theorem max_r n m : n <= m -> max n m = m.
Proof. hammer_hook "BinNat" "BinNat.N.max_r".
unfold max, le. case compare; trivial. now destruct 1.
Qed.

Lemma lt_succ_r n m : n < succ m <-> n<=m.
Proof. hammer_hook "BinNat" "BinNat.N.lt_succ_r".
destruct n as [|p], m as [|q]; simpl; try easy'.
split. now destruct p. now destruct 1.
apply Pos.lt_succ_r.
Qed.

Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

Lemma double_spec n : double n = 2 * n.
Proof. hammer_hook "BinNat" "BinNat.N.double_spec".
reflexivity.
Qed.

Lemma succ_double_spec n : succ_double n = 2 * n + 1.
Proof. hammer_hook "BinNat" "BinNat.N.succ_double_spec".
now destruct n.
Qed.

Lemma double_add n m : double (n+m) = double n + double m.
Proof. hammer_hook "BinNat" "BinNat.N.double_add".
now destruct n, m.
Qed.

Lemma succ_double_add n m : succ_double (n+m) = double n + succ_double m.
Proof. hammer_hook "BinNat" "BinNat.N.succ_double_add".
now destruct n, m.
Qed.

Lemma double_mul n m : double (n*m) = double n * m.
Proof. hammer_hook "BinNat" "BinNat.N.double_mul".
now destruct n, m.
Qed.

Lemma succ_double_mul n m :
succ_double n * m = double n * m + m.
Proof. hammer_hook "BinNat" "BinNat.N.succ_double_mul".
destruct n; simpl; destruct m; trivial.
now rewrite Pos.add_comm.
Qed.

Lemma div2_double n : div2 (double n) = n.
Proof. hammer_hook "BinNat" "BinNat.N.div2_double".
now destruct n.
Qed.

Lemma div2_succ_double n : div2 (succ_double n) = n.
Proof. hammer_hook "BinNat" "BinNat.N.div2_succ_double".
now destruct n.
Qed.

Lemma double_inj n m : double n = double m -> n = m.
Proof. hammer_hook "BinNat" "BinNat.N.double_inj".
intro H. rewrite <- (div2_double n), H. apply div2_double.
Qed.

Lemma succ_double_inj n m : succ_double n = succ_double m -> n = m.
Proof. hammer_hook "BinNat" "BinNat.N.succ_double_inj".
intro H. rewrite <- (div2_succ_double n), H. apply div2_succ_double.
Qed.

Lemma succ_double_lt n m : n<m -> succ_double n < double m.
Proof. hammer_hook "BinNat" "BinNat.N.succ_double_lt".
destruct n as [|n], m as [|m]; intros H; try easy.
unfold lt in *; simpl in *. now rewrite Pos.compare_xI_xO, H.
Qed.

Theorem compare_0_r n : (n ?= 0) <> Lt.
Proof. hammer_hook "BinNat" "BinNat.N.compare_0_r".
now destruct n.
Qed.

Lemma pow_0_r n : n ^ 0 = 1.
Proof. hammer_hook "BinNat" "BinNat.N.pow_0_r".   reflexivity. Qed.

Lemma pow_succ_r n p : 0<=p -> n^(succ p) = n * n^p.
Proof. hammer_hook "BinNat" "BinNat.N.pow_succ_r".
intros _.
destruct n, p; simpl; trivial; f_equal. apply Pos.pow_succ_r.
Qed.

Lemma pow_neg_r n p : p<0 -> n^p = 0.
Proof. hammer_hook "BinNat" "BinNat.N.pow_neg_r".
now destruct p.
Qed.

Lemma square_spec n : square n = n * n.
Proof. hammer_hook "BinNat" "BinNat.N.square_spec".
destruct n; trivial. simpl. f_equal. apply Pos.square_spec.
Qed.

Lemma size_log2 n : n<>0 -> size n = succ (log2 n).
Proof. hammer_hook "BinNat" "BinNat.N.size_log2".
destruct n as [|[n|n| ]]; trivial. now destruct 1.
Qed.

Lemma size_gt n : n < 2^(size n).
Proof. hammer_hook "BinNat" "BinNat.N.size_gt".
destruct n. reflexivity. simpl. apply Pos.size_gt.
Qed.

Lemma size_le n : 2^(size n) <= succ_double n.
Proof. hammer_hook "BinNat" "BinNat.N.size_le".
destruct n. discriminate. simpl.
change (2^Pos.size p <= Pos.succ (p~0))%positive.
apply Pos.lt_le_incl, Pos.lt_succ_r, Pos.size_le.
Qed.

Lemma log2_spec n : 0 < n ->
2^(log2 n) <= n < 2^(succ (log2 n)).
Proof. hammer_hook "BinNat" "BinNat.N.log2_spec".
destruct n as [|[p|p|]]; discriminate || intros _; simpl; split.
apply (size_le (pos p)).
apply Pos.size_gt.
apply Pos.size_le.
apply Pos.size_gt.
discriminate.
reflexivity.
Qed.

Lemma log2_nonpos n : n<=0 -> log2 n = 0.
Proof. hammer_hook "BinNat" "BinNat.N.log2_nonpos".
destruct n; intros Hn. reflexivity. now destruct Hn.
Qed.

Lemma even_spec n : even n = true <-> Even n.
Proof. hammer_hook "BinNat" "BinNat.N.even_spec".
destruct n.
split. now exists 0.
trivial.
destruct p; simpl; split; try easy.
intros (m,H). now destruct m.
now exists (pos p).
intros (m,H). now destruct m.
Qed.

Lemma odd_spec n : odd n = true <-> Odd n.
Proof. hammer_hook "BinNat" "BinNat.N.odd_spec".
destruct n.
split. discriminate.
intros (m,H). now destruct m.
destruct p; simpl; split; try easy.
now exists (pos p).
intros (m,H). now destruct m.
now exists 0.
Qed.

Theorem pos_div_eucl_spec (a:positive)(b:N) :
let (q,r) := pos_div_eucl a b in pos a = q * b + r.
Proof. hammer_hook "BinNat" "BinNat.N.pos_div_eucl_spec".
induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta.

destruct pos_div_eucl as (q,r).
change (pos a~1) with (succ_double (pos a)).
rewrite IHa, succ_double_add, double_mul.
case leb_spec; intros H; trivial.
rewrite succ_double_mul, <- add_assoc. f_equal.
now rewrite (add_comm b), sub_add.

destruct pos_div_eucl as (q,r).
change (pos a~0) with (double (pos a)).
rewrite IHa, double_add, double_mul.
case leb_spec; intros H; trivial.
rewrite succ_double_mul, <- add_assoc. f_equal.
now rewrite (add_comm b), sub_add.

now destruct b as [|[ | | ]].
Qed.

Theorem div_eucl_spec a b :
let (q,r) := div_eucl a b in a = b * q + r.
Proof. hammer_hook "BinNat" "BinNat.N.div_eucl_spec".
destruct a as [|a], b as [|b]; unfold div_eucl; trivial.
generalize (pos_div_eucl_spec a (pos b)).
destruct pos_div_eucl. now rewrite mul_comm.
Qed.

Theorem div_mod' a b : a = b * (a/b) + (a mod b).
Proof. hammer_hook "BinNat" "BinNat.N.div_mod'".
generalize (div_eucl_spec a b).
unfold div, modulo. now destruct div_eucl.
Qed.

Definition div_mod a b : b<>0 -> a = b * (a/b) + (a mod b).
Proof. hammer_hook "BinNat" "BinNat.N.div_mod".
intros _. apply div_mod'.
Qed.

Theorem pos_div_eucl_remainder (a:positive) (b:N) :
b<>0 -> snd (pos_div_eucl a b) < b.
Proof. hammer_hook "BinNat" "BinNat.N.pos_div_eucl_remainder".
intros Hb.
induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta.

destruct pos_div_eucl as (q,r); simpl in *.
case leb_spec; intros H; simpl; trivial.
apply add_lt_mono_l with b. rewrite add_comm, sub_add by trivial.
destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ].
apply (succ_double_lt _ _ IHa).

destruct pos_div_eucl as (q,r); simpl in *.
case leb_spec; intros H; simpl; trivial.
apply add_lt_mono_l with b. rewrite add_comm, sub_add by trivial.
destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ].
now destruct r.

destruct b as [|[ | | ]]; easy || (now destruct Hb).
Qed.

Theorem mod_lt a b : b<>0 -> a mod b < b.
Proof. hammer_hook "BinNat" "BinNat.N.mod_lt".
destruct b as [ |b]. now destruct 1.
destruct a as [ |a]. reflexivity.
unfold modulo. simpl. apply pos_div_eucl_remainder.
Qed.

Theorem mod_bound_pos a b : 0<=a -> 0<b -> 0 <= a mod b < b.
Proof. hammer_hook "BinNat" "BinNat.N.mod_bound_pos".
intros _ H. split. apply le_0_l. apply mod_lt. now destruct b.
Qed.

Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n.
Proof. hammer_hook "BinNat" "BinNat.N.sqrtrem_sqrt".
destruct n. reflexivity.
unfold sqrtrem, sqrt, Pos.sqrt.
destruct (Pos.sqrtrem p) as (s,r). now destruct r.
Qed.

Lemma sqrtrem_spec n :
let (s,r) := sqrtrem n in n = s*s + r /\ r <= 2*s.
Proof. hammer_hook "BinNat" "BinNat.N.sqrtrem_spec".
destruct n. now split.
generalize (Pos.sqrtrem_spec p). simpl.
destruct 1; simpl; subst; now split.
Qed.

Lemma sqrt_spec n : 0<=n ->
let s := sqrt n in s*s <= n < (succ s)*(succ s).
Proof. hammer_hook "BinNat" "BinNat.N.sqrt_spec".
intros _. destruct n. now split. apply (Pos.sqrt_spec p).
Qed.

Lemma sqrt_neg n : n<0 -> sqrt n = 0.
Proof. hammer_hook "BinNat" "BinNat.N.sqrt_neg".
now destruct n.
Qed.

Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b.
Proof. hammer_hook "BinNat" "BinNat.N.ggcd_gcd".
destruct a as [|p], b as [|q]; simpl; auto.
assert (H := Pos.ggcd_gcd p q).
destruct Pos.ggcd as (g,(aa,bb)); simpl; now f_equal.
Qed.

Lemma ggcd_correct_divisors a b :
let '(g,(aa,bb)) := ggcd a b in
a=g*aa /\ b=g*bb.
Proof. hammer_hook "BinNat" "BinNat.N.ggcd_correct_divisors".
destruct a as [|p], b as [|q]; simpl; auto.
now rewrite Pos.mul_1_r.
now rewrite Pos.mul_1_r.
generalize (Pos.ggcd_correct_divisors p q).
destruct Pos.ggcd as (g,(aa,bb)); simpl.
destruct 1; split; now f_equal.
Qed.

Lemma gcd_divide_l a b : (gcd a b | a).
Proof. hammer_hook "BinNat" "BinNat.N.gcd_divide_l".
rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b).
destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa.
now rewrite mul_comm.
Qed.

Lemma gcd_divide_r a b : (gcd a b | b).
Proof. hammer_hook "BinNat" "BinNat.N.gcd_divide_r".
rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b).
destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb.
now rewrite mul_comm.
Qed.

Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c|gcd a b).
Proof. hammer_hook "BinNat" "BinNat.N.gcd_greatest".
destruct a as [ |p], b as [ |q]; simpl; trivial.
destruct c as [ |r]. intros (s,H). destruct s; discriminate.
intros ([ |s],Hs) ([ |t],Ht); try discriminate; simpl in *.
destruct (Pos.gcd_greatest p q r) as (u,H).
exists s. now inversion Hs.
exists t. now inversion Ht.
exists (pos u). simpl; now f_equal.
Qed.

Lemma gcd_nonneg a b : 0 <= gcd a b.
Proof. hammer_hook "BinNat" "BinNat.N.gcd_nonneg".   apply le_0_l. Qed.

Lemma testbit_even_0 a : testbit (2*a) 0 = false.
Proof. hammer_hook "BinNat" "BinNat.N.testbit_even_0".
now destruct a.
Qed.

Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.
Proof. hammer_hook "BinNat" "BinNat.N.testbit_odd_0".
now destruct a.
Qed.

Lemma testbit_succ_r_div2 a n : 0<=n ->
testbit a (succ n) = testbit (div2 a) n.
Proof. hammer_hook "BinNat" "BinNat.N.testbit_succ_r_div2".
intros _. destruct a as [|[a|a| ]], n as [|n]; simpl; trivial;
f_equal; apply Pos.pred_N_succ.
Qed.

Lemma testbit_odd_succ a n : 0<=n ->
testbit (2*a+1) (succ n) = testbit a n.
Proof. hammer_hook "BinNat" "BinNat.N.testbit_odd_succ".
intros H. rewrite testbit_succ_r_div2 by trivial. f_equal. now destruct a.
Qed.

Lemma testbit_even_succ a n : 0<=n ->
testbit (2*a) (succ n) = testbit a n.
Proof. hammer_hook "BinNat" "BinNat.N.testbit_even_succ".
intros H. rewrite testbit_succ_r_div2 by trivial. f_equal. now destruct a.
Qed.

Lemma testbit_neg_r a n : n<0 -> testbit a n = false.
Proof. hammer_hook "BinNat" "BinNat.N.testbit_neg_r".
now destruct n.
Qed.

Lemma shiftr_succ_r a n :
shiftr a (succ n) = div2 (shiftr a n).
Proof. hammer_hook "BinNat" "BinNat.N.shiftr_succ_r".
destruct n; simpl; trivial. apply Pos.iter_succ.
Qed.

Lemma shiftl_succ_r a n :
shiftl a (succ n) = double (shiftl a n).
Proof. hammer_hook "BinNat" "BinNat.N.shiftl_succ_r".
destruct n, a; simpl; trivial. f_equal. apply Pos.iter_succ.
Qed.

Lemma shiftr_spec a n m : 0<=m ->
testbit (shiftr a n) m = testbit a (m+n).
Proof. hammer_hook "BinNat" "BinNat.N.shiftr_spec".
intros _. revert a m.
induction n using peano_ind; intros a m. now rewrite add_0_r.
rewrite add_comm, add_succ_l, add_comm, <- add_succ_l.
now rewrite <- IHn, testbit_succ_r_div2, shiftr_succ_r by apply le_0_l.
Qed.

Lemma shiftl_spec_high a n m : 0<=m -> n<=m ->
testbit (shiftl a n) m = testbit a (m-n).
Proof. hammer_hook "BinNat" "BinNat.N.shiftl_spec_high".
intros _ H.
rewrite <- (sub_add n m H) at 1.
set (m' := m-n). clearbody m'. clear H m. revert a m'.
induction n using peano_ind; intros a m.
rewrite add_0_r; now destruct a.
rewrite shiftl_succ_r.
rewrite add_comm, add_succ_l, add_comm.
now rewrite testbit_succ_r_div2, div2_double by apply le_0_l.
Qed.

Lemma shiftl_spec_low a n m : m<n ->
testbit (shiftl a n) m = false.
Proof. hammer_hook "BinNat" "BinNat.N.shiftl_spec_low".
revert a m.
induction n using peano_ind; intros a m H.
elim (le_0_l m). now rewrite compare_antisym, H.
rewrite shiftl_succ_r.
destruct m. now destruct (shiftl a n).
rewrite <- (succ_pos_pred p), testbit_succ_r_div2, div2_double by apply le_0_l.
apply IHn.
apply add_lt_mono_l with 1. rewrite 2 (add_succ_l 0). simpl.
now rewrite succ_pos_pred.
Qed.

Definition div2_spec a : div2 a = shiftr a 1.
Proof. hammer_hook "BinNat" "BinNat.N.div2_spec".
reflexivity.
Qed.

Lemma pos_lxor_spec p p' n :
testbit (Pos.lxor p p') n = xorb (Pos.testbit p n) (Pos.testbit p' n).
Proof. hammer_hook "BinNat" "BinNat.N.pos_lxor_spec".
revert p' n.
induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl;
(specialize (IH p'); destruct Pos.lxor; trivial; now rewrite <-IH) ||
(now destruct Pos.testbit).
Qed.

Lemma lxor_spec a a' n :
testbit (lxor a a') n = xorb (testbit a n) (testbit a' n).
Proof. hammer_hook "BinNat" "BinNat.N.lxor_spec".
destruct a, a'; simpl; trivial.
now destruct Pos.testbit.
now destruct Pos.testbit.
apply pos_lxor_spec.
Qed.

Lemma pos_lor_spec p p' n :
Pos.testbit (Pos.lor p p') n = (Pos.testbit p n) || (Pos.testbit p' n).
Proof. hammer_hook "BinNat" "BinNat.N.pos_lor_spec".
revert p' n.
induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl;
apply IH || now rewrite orb_false_r.
Qed.

Lemma lor_spec a a' n :
testbit (lor a a') n = (testbit a n) || (testbit a' n).
Proof. hammer_hook "BinNat" "BinNat.N.lor_spec".
destruct a, a'; simpl; trivial.
now rewrite orb_false_r.
apply pos_lor_spec.
Qed.

Lemma pos_land_spec p p' n :
testbit (Pos.land p p') n = (Pos.testbit p n) && (Pos.testbit p' n).
Proof. hammer_hook "BinNat" "BinNat.N.pos_land_spec".
revert p' n.
induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl;
(specialize (IH p'); destruct Pos.land; trivial; now rewrite <-IH) ||
(now rewrite andb_false_r).
Qed.

Lemma land_spec a a' n :
testbit (land a a') n = (testbit a n) && (testbit a' n).
Proof. hammer_hook "BinNat" "BinNat.N.land_spec".
destruct a, a'; simpl; trivial.
now rewrite andb_false_r.
apply pos_land_spec.
Qed.

Lemma pos_ldiff_spec p p' n :
testbit (Pos.ldiff p p') n = (Pos.testbit p n) && negb (Pos.testbit p' n).
Proof. hammer_hook "BinNat" "BinNat.N.pos_ldiff_spec".
revert p' n.
induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl;
(specialize (IH p'); destruct Pos.ldiff; trivial; now rewrite <-IH) ||
(now rewrite andb_true_r).
Qed.

Lemma ldiff_spec a a' n :
testbit (ldiff a a') n = (testbit a n) && negb (testbit a' n).
Proof. hammer_hook "BinNat" "BinNat.N.ldiff_spec".
destruct a, a'; simpl; trivial.
now rewrite andb_true_r.
apply pos_ldiff_spec.
Qed.

Include NExtraProp.

Lemma gt_lt_iff n m : n > m <-> m < n.
Proof. hammer_hook "BinNat" "BinNat.N.gt_lt_iff".
unfold lt, gt. now rewrite compare_antisym, CompOpp_iff.
Qed.

Lemma gt_lt n m : n > m -> m < n.
Proof. hammer_hook "BinNat" "BinNat.N.gt_lt".
apply gt_lt_iff.
Qed.

Lemma lt_gt n m : n < m -> m > n.
Proof. hammer_hook "BinNat" "BinNat.N.lt_gt".
apply gt_lt_iff.
Qed.

Lemma ge_le_iff n m : n >= m <-> m <= n.
Proof. hammer_hook "BinNat" "BinNat.N.ge_le_iff".
unfold le, ge. now rewrite compare_antisym, CompOpp_iff.
Qed.

Lemma ge_le n m : n >= m -> m <= n.
Proof. hammer_hook "BinNat" "BinNat.N.ge_le".
apply ge_le_iff.
Qed.

Lemma le_ge n m : n <= m -> m >= n.
Proof. hammer_hook "BinNat" "BinNat.N.le_ge".
apply ge_le_iff.
Qed.

Lemma pos_pred_shiftl_low : forall p n m, m<n ->
testbit (Pos.pred_N (Pos.shiftl p n)) m = true.
Proof. hammer_hook "BinNat" "BinNat.N.pos_pred_shiftl_low".
induction n using peano_ind.
now destruct m.
intros m H. unfold Pos.shiftl.
destruct n as [|n]; simpl in *.
destruct m. now destruct p. elim (Pos.nlt_1_r _ H).
rewrite Pos.iter_succ. simpl.
set (u:=Pos.iter xO p n) in *; clearbody u.
destruct m as [|m]. now destruct u.
rewrite <- (IHn (Pos.pred_N m)).
rewrite <- (testbit_odd_succ _ (Pos.pred_N m)).
rewrite succ_pos_pred. now destruct u.
apply le_0_l.
apply succ_lt_mono. now rewrite succ_pos_pred.
Qed.

Lemma pos_pred_shiftl_high : forall p n m, n<=m ->
testbit (Pos.pred_N (Pos.shiftl p n)) m =
testbit (shiftl (Pos.pred_N p) n) m.
Proof. hammer_hook "BinNat" "BinNat.N.pos_pred_shiftl_high".
induction n using peano_ind; intros m H.
unfold shiftl. simpl. now destruct (Pos.pred_N p).
rewrite shiftl_succ_r.
destruct n as [|n].
destruct m as [|m]. now destruct H. now destruct p.
destruct m as [|m]. now destruct H.
rewrite <- (succ_pos_pred m).
rewrite double_spec, testbit_even_succ by apply le_0_l.
rewrite <- IHn.
rewrite testbit_succ_r_div2 by apply le_0_l.
f_equal. simpl. rewrite Pos.iter_succ.
now destruct (Pos.iter xO p n).
apply succ_le_mono. now rewrite succ_pos_pred.
Qed.

Lemma pred_div2_up p : Pos.pred_N (Pos.div2_up p) = div2 (Pos.pred_N p).
Proof. hammer_hook "BinNat" "BinNat.N.pred_div2_up".
destruct p as [p|p| ]; trivial.
simpl. apply Pos.pred_N_succ.
destruct p; simpl; trivial.
Qed.

End N.

Bind Scope N_scope with N.t N.

Infix "+" := N.add : N_scope.
Infix "-" := N.sub : N_scope.
Infix "*" := N.mul : N_scope.
Infix "^" := N.pow : N_scope.

Infix "?=" := N.compare (at level 70, no associativity) : N_scope.

Infix "<=" := N.le : N_scope.
Infix "<" := N.lt : N_scope.
Infix ">=" := N.ge : N_scope.
Infix ">" := N.gt : N_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : N_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : N_scope.
Notation "x < y < z" := (x < y /\ y < z) : N_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : N_scope.

Infix "=?" := N.eqb (at level 70, no associativity) : N_scope.
Infix "<=?" := N.leb (at level 70, no associativity) : N_scope.
Infix "<?" := N.ltb (at level 70, no associativity) : N_scope.

Infix "/" := N.div : N_scope.
Infix "mod" := N.modulo (at level 40, no associativity) : N_scope.

Notation "( p | q )" := (N.divide p q) (at level 0) : N_scope.

Notation N_rect := N_rect (only parsing).
Notation N_rec := N_rec (only parsing).
Notation N_ind := N_ind (only parsing).
Notation N0 := N0 (only parsing).
Notation Npos := N.pos (only parsing).

Notation Ndiscr := N.discr (compat "8.3").
Notation Ndouble_plus_one := N.succ_double (compat "8.3").
Notation Ndouble := N.double (compat "8.3").
Notation Nsucc := N.succ (compat "8.3").
Notation Npred := N.pred (compat "8.3").
Notation Nsucc_pos := N.succ_pos (compat "8.3").
Notation Ppred_N := Pos.pred_N (compat "8.3").
Notation Nplus := N.add (compat "8.3").
Notation Nminus := N.sub (compat "8.3").
Notation Nmult := N.mul (compat "8.3").
Notation Neqb := N.eqb (compat "8.3").
Notation Ncompare := N.compare (compat "8.3").
Notation Nlt := N.lt (compat "8.3").
Notation Ngt := N.gt (compat "8.3").
Notation Nle := N.le (compat "8.3").
Notation Nge := N.ge (compat "8.3").
Notation Nmin := N.min (compat "8.3").
Notation Nmax := N.max (compat "8.3").
Notation Ndiv2 := N.div2 (compat "8.3").
Notation Neven := N.even (compat "8.3").
Notation Nodd := N.odd (compat "8.3").
Notation Npow := N.pow (compat "8.3").
Notation Nlog2 := N.log2 (compat "8.3").

Notation nat_of_N := N.to_nat (compat "8.3").
Notation N_of_nat := N.of_nat (compat "8.3").
Notation N_eq_dec := N.eq_dec (compat "8.3").
Notation Nrect := N.peano_rect (compat "8.3").
Notation Nrect_base := N.peano_rect_base (compat "8.3").
Notation Nrect_step := N.peano_rect_succ (compat "8.3").
Notation Nind := N.peano_ind (compat "8.3").
Notation Nrec := N.peano_rec (compat "8.3").
Notation Nrec_base := N.peano_rec_base (compat "8.3").
Notation Nrec_succ := N.peano_rec_succ (compat "8.3").

Notation Npred_succ := N.pred_succ (compat "8.3").
Notation Npred_minus := N.pred_sub (compat "8.3").
Notation Nsucc_pred := N.succ_pred (compat "8.3").
Notation Ppred_N_spec := N.pos_pred_spec (compat "8.3").
Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.3").
Notation Ppred_Nsucc := N.pos_pred_succ (compat "8.3").
Notation Nplus_0_l := N.add_0_l (compat "8.3").
Notation Nplus_0_r := N.add_0_r (compat "8.3").
Notation Nplus_comm := N.add_comm (compat "8.3").
Notation Nplus_assoc := N.add_assoc (compat "8.3").
Notation Nplus_succ := N.add_succ_l (compat "8.3").
Notation Nsucc_0 := N.succ_0_discr (compat "8.3").
Notation Nsucc_inj := N.succ_inj (compat "8.3").
Notation Nminus_N0_Nle := N.sub_0_le (compat "8.3").
Notation Nminus_0_r := N.sub_0_r (compat "8.3").
Notation Nminus_succ_r:= N.sub_succ_r (compat "8.3").
Notation Nmult_0_l := N.mul_0_l (compat "8.3").
Notation Nmult_1_l := N.mul_1_l (compat "8.3").
Notation Nmult_1_r := N.mul_1_r (compat "8.3").
Notation Nmult_comm := N.mul_comm (compat "8.3").
Notation Nmult_assoc := N.mul_assoc (compat "8.3").
Notation Nmult_plus_distr_r := N.mul_add_distr_r (compat "8.3").
Notation Neqb_eq := N.eqb_eq (compat "8.3").
Notation Nle_0 := N.le_0_l (compat "8.3").
Notation Ncompare_refl := N.compare_refl (compat "8.3").
Notation Ncompare_Eq_eq := N.compare_eq (compat "8.3").
Notation Ncompare_eq_correct := N.compare_eq_iff (compat "8.3").
Notation Nlt_irrefl := N.lt_irrefl (compat "8.3").
Notation Nlt_trans := N.lt_trans (compat "8.3").
Notation Nle_lteq := N.lt_eq_cases (compat "8.3").
Notation Nlt_succ_r := N.lt_succ_r (compat "8.3").
Notation Nle_trans := N.le_trans (compat "8.3").
Notation Nle_succ_l := N.le_succ_l (compat "8.3").
Notation Ncompare_spec := N.compare_spec (compat "8.3").
Notation Ncompare_0 := N.compare_0_r (compat "8.3").
Notation Ndouble_div2 := N.div2_double (compat "8.3").
Notation Ndouble_plus_one_div2 := N.div2_succ_double (compat "8.3").
Notation Ndouble_inj := N.double_inj (compat "8.3").
Notation Ndouble_plus_one_inj := N.succ_double_inj (compat "8.3").
Notation Npow_0_r := N.pow_0_r (compat "8.3").
Notation Npow_succ_r := N.pow_succ_r (compat "8.3").
Notation Nlog2_spec := N.log2_spec (compat "8.3").
Notation Nlog2_nonpos := N.log2_nonpos (compat "8.3").
Notation Neven_spec := N.even_spec (compat "8.3").
Notation Nodd_spec := N.odd_spec (compat "8.3").
Notation Nlt_not_eq := N.lt_neq (compat "8.3").
Notation Ngt_Nlt := N.gt_lt (compat "8.3").

Lemma Nplus_reg_l n m p : n + m = n + p -> m = p.
Proof. hammer_hook "BinNat" "BinNat.Nplus_reg_l".  exact ((proj1 (N.add_cancel_l m p n))). Qed.
Lemma Nmult_Sn_m n m : N.succ n * m = m + n * m.
Proof. hammer_hook "BinNat" "BinNat.Nmult_Sn_m".  exact ((eq_trans (N.mul_succ_l n m) (N.add_comm _ _))). Qed.
Lemma Nmult_plus_distr_l n m p : p * (n + m) = p * n + p * m.
Proof. hammer_hook "BinNat" "BinNat.Nmult_plus_distr_l".  exact ((N.mul_add_distr_l p n m)). Qed.
Lemma Nmult_reg_r n m p : p <> 0 -> n * p = m * p -> n = m.
Proof. hammer_hook "BinNat" "BinNat.Nmult_reg_r".  exact ((fun H => proj1 (N.mul_cancel_r n m p H))). Qed.
Lemma Ncompare_antisym n m : CompOpp (n ?= m) = (m ?= n).
Proof. hammer_hook "BinNat" "BinNat.Ncompare_antisym".  exact ((eq_sym (N.compare_antisym n m))). Qed.

Definition N_ind_double a P f0 f2 fS2 := N.binary_ind P f0 f2 fS2 a.
Definition N_rec_double a P f0 f2 fS2 := N.binary_rec P f0 f2 fS2 a.

author: lukaszcz

repo: coqhammer-eval


text:
Require Import ZArith Lia MyNat Div2.

(** Finite and computable subsets of [nat], by functions in [nat -> bool] *)

(** Tactics *)

Ltac rem t x Hx :=
  pose (x := t); assert (Hx : x = t) by reflexivity;
    try rewrite <- Hx in *; clearbody x.

Ltac destruct_if t :=
  lazymatch t with
  | if ?t then _ else _ =>
      let Eqb := fresh "Eqb" in
      let b := fresh "b" in
      rem t b Eqb; destruct b
  | ?u ?v => destruct_if u || destruct_if v
  end.

Ltac auto_if :=
  match goal with
  | |- ?T => destruct_if T
  | H : ?T |- _ => destruct_if T
  end.

Ltac impossible := exfalso; discriminate || lia || tauto.

Ltac dumb_aux :=
  auto || auto with * || discriminate
  || intuition || tauto || lia.

Ltac dumb :=
  try solve
    [ impossible
    | subst; dumb_aux || (simpl in *; dumb_aux)
    | intros; dumb_aux || (simpl in *; dumb_aux) ].

(** * Basic operations and types *)

Definition bset := nat -> bool.

Definition singleton (x : nat) : bset :=
  fun y => if eq_nat_dec x y then true else false.

Definition inter (P Q : bset) : bset := fun i => andb (P i) (Q i).

Definition union (P Q : bset) : bset := fun i => orb (P i) (Q i).

(** Bounded cardinal *)

Definition IBN : bool -> nat := fun b => (if b then 1 else 0)%nat.

Fixpoint count n P :=
  match n with
  | O => O
  | S n => (IBN (P n) + count n P)%nat
  end.

(** Comparison *)

Definition same (P Q : bset) : Prop := forall i, P i = Q i.

Fixpoint same_bool n P Q :=
  match n with
  | O => true
  | S n => if Bool.eqb (P n) (Q n) then same_bool n P Q else false
  end.

(* TODO les typesclasses peuvent nous aider ? *)

Lemma same_true n P Q : same_bool n P Q = true -> forall i, i < n -> P i = Q i.
Proof.
  induction n; intros E i L.
    impossible.

    simpl in E.
    auto_if; dumb.
    destruct (eq_nat_dec i n); dumb.
    apply Bool.eqb_true_iff.
    subst; dumb.
Qed.

Lemma same_false n P Q : same_bool n P Q = false -> { i | i < n /\ P i <> Q i }.
Proof.
  induction n; simpl; intros I.
    impossible.

    remember (Bool.eqb (P n) (Q n)) as b.
    destruct b.
      destruct IHn as (i, (Li, Di)); eauto.
      destruct (Bool.eqb_false_iff (P n) (Q n)); eauto.
Qed.

(* This lemma is a corollary of the next one that is more elegant. TODO *)

Lemma count_union_inter n P Q : (count n (union P Q) + count n (inter P Q) =
  count n P + count n Q)%nat.
Proof.
  induction n; auto; simpl.
  unfold IBN, union, inter in *.
  remember (P n) as Pn; remember (Q n) as Qn.
  destruct Pn; destruct Qn; simpl; lia.
Qed.

Lemma not_empty P n : O < count n P -> { i | i < n /\ P i = true }.
Proof.
  intros CP.
  induction n.
    simpl in CP; impossible.

    simpl in CP.
    rem (P n) Pn EPn; destruct Pn.
      exists n; auto.

      destruct IHn as (i, Hi); dumb.
      exists i; dumb.
Defined.

Lemma count_union n P Q : count n (union P Q) =
  count n P + count n Q - count n (inter P Q).
Proof.
  rewrite <- count_union_inter.
  auto with *.
Qed.

Lemma count_inter n P Q : count n (inter P Q) =
  count n P + count n Q - count n (union P Q).
Proof.
  rewrite <- count_union_inter.
  auto with *.
Qed.

Lemma count_bound P n : count n P <= n.
Proof.
  induction n.
    dumb.
    simpl; destruct (P n); dumb.
Qed.

Lemma count_drawers : forall P Q n,
  n < count n P + count n Q -> { i | i < n /\ P i = true /\ Q i = true }.
Proof.
  intros P Q n L.
  destruct (not_empty (inter P Q) n) as (i, Hi).
    rewrite count_inter.
    pose proof count_bound (union P Q) n.
    lia.

    exists i; intuition; unfold inter in *;
      destruct (P i); destruct (Q i); intuition.
Defined.

Definition injective domain (f : nat -> nat) := forall i j,
  i < domain -> j < domain -> f i = f j -> i = j.

Definition bounded domain bound (f : nat -> nat) := forall i, i < domain -> f i < bound.

Fixpoint has_antecedent (f : nat -> nat) domain y :=
  match domain with
  | O => false
  | S domain => if eq_nat_dec (f domain) y then true else has_antecedent f domain y
  end.

(* TODO delete def ? *)
Fixpoint number_of_pals_____OUT (f : nat -> nat) domain x :=
  match domain with
  | O => 0
  | S domain => (if eq_nat_dec (f domain) (f x) then 1 else 0) + number_of_pals_____OUT f domain x
  end.

(** [image f dom] is the set f({0, ..., dom-1}) *)
Definition image (f : nat -> nat) domain : bset := has_antecedent f domain.

Lemma image_true f dom y :
  image f dom y = true -> { i | i < dom /\ f i = y }.
Proof.
  induction dom; intros A; dumb.
  destruct (eq_nat_dec (f dom) y) as [E|E].
    exists dom; eauto.

    destruct IHdom as (i, Hi).
      simpl in A.
      auto_if; dumb.

      exists i; dumb.
Defined.

Lemma image_false : forall f domain y,
  image f domain y = false -> forall x, x < domain -> f x = y -> False.
Proof.
  intros f dom; induction dom; intros y T x Bx Exy.
    inversion Bx.

    simpl in T.
    auto_if; dumb.
      apply (IHdom y T x); dumb.
      cut (x <> dom); dumb.
Qed.

Lemma image_true_pr f dom y :
  forall i, i < dom -> y = f i -> image f dom y = true.
Proof.
  intros i L E.
  remember (image f dom y) as b; symmetry in Heqb.
  destruct b; [ reflexivity | exfalso ].
  exfalso; eapply image_false; eauto.
Qed.

Lemma image_false_pr f dom y :
  (forall i, i < dom -> y <> f i) -> image f dom y = false.
Proof.
  intros NE.
  remember (image f dom y) as b; symmetry in Heqb.
  destruct b; [ exfalso | reflexivity ].
  destruct (image_true _ _ _ Heqb) as (n, Hn).
  specialize (NE n); intuition.
Qed.

Fixpoint sum n f := match n with O => O | S n => f n + sum n f end.

Definition is_duplicate f n := IBN (has_antecedent f n (f n)).

Definition is_duplicate_outside f bound n :=
  if lt_dec bound (f n) then IBN (has_antecedent f n (f n)) else O.

(** TODO unifier l'ordre des variables bound/domain *)

Fixpoint count_outside domain bound f :=
  match domain with
  | O => O
  | S domain => (if lt_dec (f domain) bound then 1 else 0) + count_outside domain bound f
  end.

(*
Lemma count_image : forall domain bound f,
  count bound (image f domain)
  + sum domain (is_duplicate f)
  = domain
  + sum domain (is_duplicate_outside f bound).
Proof.
  intros.
  replace f with div2.
  replace domain with 24%nat.
  replace bound with 5%nat.
  simpl count; simpl sum.
  idtac "utilise un dessin !".
  fail.
  simpl.

  intros domain bound f; induction domain.
    clear; induction bound; auto with *.

    simpl.
    rewrite (plus_comm domain), <- plus_assoc, (plus_comm _ domain).
    rewrite <- IHdomain; clear.
    induction bound.
      simpl.
      induction domain.
        simpl.
    unfold is_duplicate, is_duplicate_outside.
    destruct (lt_dec (f domain) bound) as [L|NL].
      repeat rewrite plus_assoc.
      rewrite (plus_comm _ 1).
      rewrite <- (plus_assoc 1), <- IHdomain.
        simpl.
    remember (f domain) as y0.

        intros i; auto.

      rewrite IHdomain.
    clear IHdomain.

(*
  intros domain bound f; induction bound.
    auto.

    simpl.
    rewrite <- IHbound.
    f_equal.
    clear.
    induction domain.
      auto.

      simpl.
      rewrite IHdomain.
      rewrite plus_comm.
      f_equal.
      destruct (eq_nat_dec (f bound) domain).
*)
  intros domain bound f Bf; induction domain.
    clear; induction bound; auto.
    (***
Ça ne marche pas il faut faire une partie du membre gauche qui
compte aussi les points qui ne sont pas dans l'image (quand f pas bornée
par [bound])

On a une partie "is_duplicate" qui parle de l'injectivité

Il faut faire une partie "count outside" qui parle de la bornitude
***)
    simpl.
    simpl; rewrite IHdomain.
    clear.
    induction bound.
      auto.

      simpl.
      rewrite <- IHbound.
      repeat rewrite plus_assoc.

      f_equal.
      rewrite plus_comm.
      f_equal.

      destruct (eq_nat_dec (f domain) bound).
        exfalso.

        simpl.
        auto.

      destruct (eq_nat_dec (f bound) domain).
        simpl.
      simpl.
        simpl.
    f_equal.
    assert (forall a b c d, a = b ) as App; apply App; clear App.
    Require Import Arith.
    apply plus_reg.
Qed.
*)

Lemma image_injective_plus_one : forall domain f,
  same (image f (S domain)) (union (image f domain) (singleton (f domain))).
Proof.
  intros dom f i.
  unfold union, singleton.
  simpl; auto_if; auto with *.
Qed.

(* The converse is true, but osef. *)
Lemma count_same S T : same S T -> forall n, count n S = count n T.
Proof.
  intros E n; induction n; simpl; dumb.
  rewrite E; dumb.
Qed.

Lemma count_same_bounded S T n : (forall i, i < n -> S i = T i) -> count n S = count n T.
Proof.
  intros E; induction n; simpl; dumb.
  repeat (f_equal; dumb).
Qed.

Lemma count_union_singleton P a n :
  P a = false -> a < n ->
    count n (union P (singleton a)) = S (count n P).
Proof.
  intros Ma L.
  induction n; dumb.
  unfold union, singleton; simpl.
  destruct (eq_nat_dec a n).
    subst; rewrite Ma; simpl.
    f_equal; apply count_same_bounded; intros i Li.
    auto_if; dumb.

    rewrite plus_n_Sm, <- IHn; dumb.
    repeat f_equal; auto with *.
Qed.

Lemma count_image_injective_plus_one : forall domain f bound,
  injective (S domain) f -> bounded (S domain) bound f ->
    count bound (image f (S domain)) = S (count bound (image f domain)).
Proof.
  intros dom f M If Bf.
  pose proof image_injective_plus_one dom f as HS.
  erewrite count_same; [ | eassumption ].
  rewrite count_union_singleton; dumb.
    apply image_false_pr; intros i L E.
    apply If in E; dumb.
Qed.

Lemma injective_S dom f : injective (S dom) f -> injective dom f.
Proof.
  intros If i j Bi Bj.
  apply If; dumb.
Qed.

Lemma bounded_S dom M f : bounded (S dom) M f -> bounded dom M f.
Proof.
  intros If i Bi.
  apply If; dumb.
Qed.

Lemma count_image_injective : forall domain bound f,
  injective domain f -> bounded domain bound f ->
    count bound (image f domain) = domain.
Proof.
  intros dom M f Injf Bf.
  induction dom.
    simpl; clear.
    induction M; auto.

    rewrite count_image_injective_plus_one; dumb.
    rewrite IHdom; dumb.
      apply injective_S; auto.
      apply bounded_S; auto.
Qed.

(*
Fact example :
  let A := (fun x => if lt_dec x 20 then true else false) in
  let B := (fun x => if lt_dec 18 x then true else false) in
  { i | inter A B i = true }.
Proof.
  intros.
  cut { i | i < 100 /\ inter A B i = true}.
    intros (i, []); exists i; eauto.

  apply not_empty.
  auto.
Defined.

Eval compute in projT1 example.
*)

(*
Record natset := mknatset { natset_bound : nat; natset_charact : nat -> bool }.

Definition mknatset_dec n P (Pdec : nat_decidable P) :=
  mknatset n (nat_dec_bool P Pdec).

Program Definition image n m (f : nat -> nat) : natset :=
  mknatset_dec m (fun y => { x | y = f x /\ x < n}) _.
Next Obligation.
  intros y.
  induction n.
    right; intros (x, (_, I)); inversion I.
    destruct (eq_nat_dec (f n) y) as [E|E].
      left; exists n; eauto.
      destruct IHn as [(x, (Hxy, Bx)) | I].
        left; exists x; eauto.
        right; intros (x, (Hxy, Bx)); apply I; exists x; split.
          auto.
          destruct (eq_nat_dec x n) as [G|G].
            subst; tauto.
            lia.
Defined.

Definition card (S : natset) := count (natset_bound S) (natset_charact S).

Lemma card_image_injective : forall n m f,
  injective n f -> bound n m f ->
    card (image n m f) = n.
Proof.
  intros n m; generalize n; clear n; induction m; intros n f If Bf.
    compute.
    destruct n; auto.
    specialize (Bf O (lt_O_Sn _)); inversion Bf.

    unfold card, image, image_obligation_1 (*ouch*).
    simpl.
    unfold nat_dec_bool.
    (* arf *)

*)

author: coq-community

repo: coqtail-math


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 INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Correctness of instruction selection *)

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Cminor.
Require Import Op.
Require Import CminorSel.
Require Import SelectOp.
Require Import Selection.
Require Import SelectOpproof.
Require Import BuiltinFunctions.

Open Local Scope cminorsel_scope.

Section WITHMEM.
Context `{Hcc: CompilerConfiguration}.

(** * Correctness of the instruction selection functions for expressions *)

Section CMCONSTR.

Variable ge: genv.
Variable sp: val.
Variable e: env.
Variable m: mem.

Lemma eval_condition_of_expr:
  forall le a v b,
  eval_expr ge sp e m le a v ->
  Val.bool_of_val v b ->
  match condition_of_expr a with (cond, args) =>
    exists vl,
    eval_exprlist ge sp e m le args vl /\
    eval_condition cond vl m = Some b
  end.
Proof.
  intros until a. functional induction (condition_of_expr a); intros.
(* compare *)
  inv H. exists vl; split; auto.
  simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto.
(* default *)
  exists (v :: nil); split. constructor. auto. constructor.
  simpl. inv H0. auto. auto.
Qed.

Lemma eval_load:
  forall le a v chunk v',
  eval_expr ge sp e m le a v ->
  Mem.loadv chunk m v = Some v' ->
  eval_expr ge sp e m le (load chunk a) v'.
Proof.
  intros. generalize H0; destruct v; simpl; intro; try discriminate.
  unfold load.
  generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)).
  destruct (addressing chunk a). intros [vl [EV EQ]].
  eapply eval_Eload; eauto.
Qed.

Lemma eval_store:
  forall chunk a1 a2 v1 v2 f k m',
  eval_expr ge sp e m nil a1 v1 ->
  eval_expr ge sp e m nil a2 v2 ->
  Mem.storev chunk m v1 v2 = Some m' ->
  step ge (State f (store chunk a1 a2) k sp e m)
       E0 (State f Sskip k sp e m').
Proof.
  intros. generalize H1; destruct v1; simpl; intro; try discriminate.
  unfold store.
  generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)).
  destruct (addressing chunk a1). intros [vl [EV EQ]].
  eapply step_store; eauto.
Qed.

(** Correctness of instruction selection for operators *)

Lemma eval_sel_unop:
  forall le op a1 v1 v,
  eval_expr ge sp e m le a1 v1 ->
  eval_unop op v1 = Some v ->
  exists v', eval_expr ge sp e m le (sel_unop op a1) v' /\ Val.lessdef v v'.
Proof.
  destruct op; simpl; intros; FuncInv; try subst v.
  apply eval_cast8unsigned; auto.
  apply eval_cast8signed; auto.
  apply eval_cast16unsigned; auto.
  apply eval_cast16signed; auto.
  apply eval_negint; auto.
  apply eval_notint; auto.
  apply eval_negf; auto.
  apply eval_absf; auto.
  apply eval_singleoffloat; auto.
  eapply eval_intoffloat; eauto.
  eapply eval_intuoffloat; eauto.
  eapply eval_floatofint; eauto.
  eapply eval_floatofintu; eauto.
Qed.

Lemma eval_sel_binop:
  forall le op a1 a2 v1 v2 v,
  eval_expr ge sp e m le a1 v1 ->
  eval_expr ge sp e m le a2 v2 ->
  eval_binop op v1 v2 m = Some v ->
  exists v', eval_expr ge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'.
Proof.
  destruct op; simpl; intros; FuncInv; try subst v.
  apply eval_add; auto.
  apply eval_sub; auto.
  apply eval_mul; auto.
  eapply eval_divs; eauto.
  eapply eval_divu; eauto.
  eapply eval_mods; eauto.
  eapply eval_modu; eauto.
  apply eval_and; auto.
  apply eval_or; auto.
  apply eval_xor; auto.
  apply eval_shl; auto.
  apply eval_shr; auto.
  apply eval_shru; auto.
  apply eval_addf; auto.
  apply eval_subf; auto.
  apply eval_mulf; auto.
  apply eval_divf; auto.
  apply eval_comp; auto.
  apply eval_compu; auto.
  apply eval_compf; auto.
Qed.

End CMCONSTR.

(** Recognition of calls to built-in functions *)

Lemma expr_is_addrof_ident_correct:
  forall e id,
  expr_is_addrof_ident e = Some id ->
  e = Cminor.Econst (Cminor.Oaddrsymbol id Int.zero).
Proof.
  intros e id. unfold expr_is_addrof_ident.
  destruct e; try congruence.
  destruct c; try congruence.
  predSpec Int.eq Int.eq_spec i0 Int.zero; congruence.
Qed.

Lemma classify_call_correct:
  forall ge sp e m a v fd,
  Cminor.eval_expr ge sp e m a v ->
  Genv.find_funct ge v = Some fd ->
  match classify_call ge a with
  | Call_default => True
  | Call_imm id => exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b Int.zero
  end.
Proof.
  unfold classify_call; intros.
  destruct (expr_is_addrof_ident a) as [id|] eqn:?.
  exploit expr_is_addrof_ident_correct; eauto. intros EQ; subst a.
  inv H. inv H2.
  destruct (Genv.find_symbol ge id) as [b|] eqn:?.
  eauto.
  simpl in H0. discriminate.
  auto.
Qed.

(** Compatibility of evaluation functions with the "less defined than" relation. *)

Ltac TrivialExists :=
  match goal with
  | [ |- exists v, Some ?x = Some v /\ _ ] => exists x; split; auto
  | _ => idtac
  end.

Lemma eval_unop_lessdef:
  forall op v1 v1' v,
  eval_unop op v1 = Some v -> Val.lessdef v1 v1' ->
  exists v', eval_unop op v1' = Some v' /\ Val.lessdef v v'.
Proof.
  intros until v; intros EV LD. inv LD.
  exists v; auto.
  destruct op; simpl in *; inv EV; TrivialExists.
Qed.

Lemma eval_binop_lessdef:
  forall op v1 v1' v2 v2' v m m',
  eval_binop op v1 v2 m = Some v ->
  Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Mem.extends m m' ->
  exists v', eval_binop op v1' v2' m' = Some v' /\ Val.lessdef v v'.
Proof.
  intros until m'; intros EV LD1 LD2 ME.
  assert (exists v', eval_binop op v1' v2' m = Some v' /\ Val.lessdef v v').
  inv LD1. inv LD2. exists v; auto.
  destruct op; destruct v1'; simpl in *; inv EV; TrivialExists.
  destruct op; simpl in *; inv EV; TrivialExists.
  destruct op; try (exact H).
  simpl in *. TrivialExists. inv EV. apply Val.of_optbool_lessdef.
  intros. apply Val.cmpu_bool_lessdef with (Mem.valid_pointer m) v1 v2; auto.
  intros; eapply Mem.valid_pointer_extends; eauto.
Qed.

(** * Semantic preservation for instruction selection. *)

Section PRESERVATION.

Variable prog: Cminor.program.
Let tprog := sel_program prog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

(** Relationship between the global environments for the original
  Cminor program and the generated CminorSel program. *)

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  intros; unfold ge, tge, tprog, sel_program.
  apply Genv.find_symbol_transf.
Qed.

Lemma function_ptr_translated:
  forall (b: block) (f: Cminor.fundef),
  Genv.find_funct_ptr ge b = Some f ->
  Genv.find_funct_ptr tge b = Some (sel_fundef ge f).
Proof.
  intros.
  exact (Genv.find_funct_ptr_transf (sel_fundef ge) _ _ H).
Qed.

Lemma functions_translated:
  forall (v v': val) (f: Cminor.fundef),
  Genv.find_funct ge v = Some f ->
  Val.lessdef v v' ->
  Genv.find_funct tge v' = Some (sel_fundef ge f).
Proof.
  intros. inv H0.
  exact (Genv.find_funct_transf (sel_fundef ge) _ _ H).
  simpl in H. discriminate.
Qed.

Lemma sig_function_translated:
  forall f,
  funsig (sel_fundef ge f) = Cminor.funsig f.
Proof.
  intros. destruct f; reflexivity.
Qed.

Lemma varinfo_preserved:
  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
Proof.
  intros; unfold ge, tge, tprog, sel_program.
  apply Genv.find_var_info_transf.
Qed.

(** Relationship between the local environments. *)

Definition env_lessdef (e1 e2: env) : Prop :=
  forall id v1, e1!id = Some v1 -> exists v2, e2!id = Some v2 /\ Val.lessdef v1 v2.

Lemma set_var_lessdef:
  forall e1 e2 id v1 v2,
  env_lessdef e1 e2 -> Val.lessdef v1 v2 ->
  env_lessdef (PTree.set id v1 e1) (PTree.set id v2 e2).
Proof.
  intros; red; intros. rewrite PTree.gsspec in *. destruct (peq id0 id).
  exists v2; split; congruence.
  auto.
Qed.

Lemma set_params_lessdef:
  forall il vl1 vl2,
  Val.lessdef_list vl1 vl2 ->
  env_lessdef (set_params vl1 il) (set_params vl2 il).
Proof.
  induction il; simpl; intros.
  red; intros. rewrite PTree.gempty in H0; congruence.
  inv H; apply set_var_lessdef; auto.
Qed.

Lemma set_locals_lessdef:
  forall e1 e2, env_lessdef e1 e2 ->
  forall il, env_lessdef (set_locals il e1) (set_locals il e2).
Proof.
  induction il; simpl. auto. apply set_var_lessdef; auto.
Qed.

(** Semantic preservation for expressions. *)

Lemma sel_expr_correct:
  forall sp e m a v,
  Cminor.eval_expr ge sp e m a v ->
  forall e' le m',
  env_lessdef e e' -> Mem.extends m m' ->
  exists v', eval_expr tge sp e' m' le (sel_expr a) v' /\ Val.lessdef v v'.
Proof.
  induction 1; intros; simpl.
  (* Evar *)
  exploit H0; eauto. intros [v' [A B]]. exists v'; split; auto. constructor; auto.
  (* Econst *)
  destruct cst; simpl in *; inv H.
  exists (Vint i); split; auto. econstructor. constructor. auto.
  exists (Vfloat f); split; auto. econstructor. constructor. auto.
  rewrite <- symbols_preserved. fold (symbol_address tge i i0). apply eval_addrsymbol.
  apply eval_addrstack.
  (* Eunop *)
  exploit IHeval_expr; eauto. intros [v1' [A B]].
  exploit eval_unop_lessdef; eauto. intros [v' [C D]].
  exploit eval_sel_unop; eauto. intros [v'' [E F]].
  exists v''; split; eauto. eapply Val.lessdef_trans; eauto.
  (* Ebinop *)
  exploit IHeval_expr1; eauto. intros [v1' [A B]].
  exploit IHeval_expr2; eauto. intros [v2' [C D]].
  exploit eval_binop_lessdef; eauto. intros [v' [E F]].
  exploit eval_sel_binop. eexact A. eexact C. eauto. intros [v'' [P Q]].
  exists v''; split; eauto. eapply Val.lessdef_trans; eauto.
  (* Eload *)
  exploit IHeval_expr; eauto. intros [vaddr' [A B]].
  exploit Mem.loadv_extends; eauto. intros [v' [C D]].
  exists v'; split; auto. eapply eval_load; eauto.
Qed.

Lemma sel_exprlist_correct:
  forall sp e m a v,
  Cminor.eval_exprlist ge sp e m a v ->
  forall e' le m',
  env_lessdef e e' -> Mem.extends m m' ->
  exists v', eval_exprlist tge sp e' m' le (sel_exprlist a) v' /\ Val.lessdef_list v v'.
Proof.
  induction 1; intros; simpl.
  exists (@nil val); split; auto. constructor.
  exploit sel_expr_correct; eauto. intros [v1' [A B]].
  exploit IHeval_exprlist; eauto. intros [vl' [C D]].
  exists (v1' :: vl'); split; auto. constructor; eauto.
Qed.

(** Semantic preservation for functions and statements. *)

Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop :=
  | match_cont_stop:
      match_cont Cminor.Kstop Kstop
  | match_cont_seq: forall s k k',
      match_cont k k' ->
      match_cont (Cminor.Kseq s k) (Kseq (sel_stmt ge s) k')
  | match_cont_block: forall k k',
      match_cont k k' ->
      match_cont (Cminor.Kblock k) (Kblock k')
  | match_cont_call: forall id f sp e k e' k',
      match_cont k k' -> env_lessdef e e' ->
      match_cont (Cminor.Kcall id f sp e k) (Kcall id (sel_function ge f) sp e' k').

Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
  | match_state: forall f s k s' k' sp e m e' m',
      s' = sel_stmt ge s ->
      match_cont k k' ->
      env_lessdef e e' ->
      Mem.extends m m' ->
      match_states
        (Cminor.State f s k sp e m)
        (State (sel_function ge f) s' k' sp e' m')
  | match_callstate: forall f args args' k k' m m',
      match_cont k k' ->
      Val.lessdef_list args args' ->
      Mem.extends m m' ->
      match_states
        (Cminor.Callstate f args k m)
        (Callstate (sel_fundef ge f) args' k' m')
  | match_returnstate: forall v v' k k' m m',
      match_cont k k' ->
      Val.lessdef v v' ->
      Mem.extends m m' ->
      match_states
        (Cminor.Returnstate v k m)
        (Returnstate v' k' m').

Remark call_cont_commut:
  forall k k', match_cont k k' -> match_cont (Cminor.call_cont k) (call_cont k').
Proof.
  induction 1; simpl; auto. constructor. constructor; auto.
Qed.

Remark find_label_commut:
  forall lbl s k k',
  match_cont k k' ->
  match Cminor.find_label lbl s k, find_label lbl (sel_stmt ge s) k' with
  | None, None => True
  | Some(s1, k1), Some(s1', k1') => s1' = sel_stmt ge s1 /\ match_cont k1 k1'
  | _, _ => False
  end.
Proof.
  induction s; intros; simpl; auto.
(* store *)
  unfold store. destruct (addressing m (sel_expr e)); simpl; auto.
(* call *)
  destruct (classify_call ge e); simpl; auto.
(* tailcall *)
  destruct (classify_call ge e); simpl; auto.
(* seq *)
  exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto.
  destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ];
  destruct (find_label lbl (sel_stmt ge s1) (Kseq (sel_stmt ge s2) k')) as [[sy ky] | ];
  intuition. apply IHs2; auto.
(* ifthenelse *)
  destruct (condition_of_expr (sel_expr e)) as [cond args]. simpl.
  exploit (IHs1 k); eauto.
  destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ];
  destruct (find_label lbl (sel_stmt ge s1) k') as [[sy ky] | ];
  intuition. apply IHs2; auto.
(* loop *)
  apply IHs. constructor; auto.
(* block *)
  apply IHs. constructor; auto.
(* return *)
  destruct o; simpl; auto.
(* label *)
  destruct (ident_eq lbl l). auto. apply IHs; auto.
Qed.

Definition measure (s: Cminor.state) : nat :=
  match s with
  | Cminor.Callstate _ _ _ _ => 0%nat
  | Cminor.State _ _ _ _ _ _ => 1%nat
  | Cminor.Returnstate _ _ _ => 2%nat
  end.

Lemma sel_step_correct:
  forall S1 t S2, Cminor.step ge S1 t S2 ->
  forall T1, match_states S1 T1 ->
  (exists T2, step tge T1 t T2 /\ match_states S2 T2)
  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat.
Proof.
  induction 1; intros T1 ME; inv ME; simpl.
  (* skip seq *)
  inv H7. left; econstructor; split. econstructor. constructor; auto.
  (* skip block *)
  inv H7. left; econstructor; split. econstructor. constructor; auto.
  (* skip call *)
  exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
  left; econstructor; split.
  econstructor. inv H9; simpl in H; simpl; auto.
  eauto.
  constructor; auto.
  (* assign *)
  exploit sel_expr_correct; eauto. intros [v' [A B]].
  left; econstructor; split.
  econstructor; eauto.
  constructor; auto. apply set_var_lessdef; auto.
  (* store *)
  exploit sel_expr_correct. eexact H. eauto. eauto. intros [vaddr' [A B]].
  exploit sel_expr_correct. eexact H0. eauto. eauto. intros [v' [C D]].
  exploit Mem.storev_extends; eauto. intros [m2' [P Q]].
  left; econstructor; split.
  eapply eval_store; eauto.
  constructor; auto.
  (* Scall *)
  exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
  exploit classify_call_correct; eauto.
  destruct (classify_call ge a) as [ | id].
  (* indirect *)
  exploit sel_expr_correct; eauto. intros [vf' [A B]].
  left; econstructor; split.
  econstructor; eauto. econstructor; eauto.
  eapply functions_translated; eauto.
  apply sig_function_translated.
  constructor; auto. constructor; auto.
  (* direct *)
  intros [b [U V]].
  left; econstructor; split.
  econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto.
  eapply functions_translated; eauto. subst vf; auto.
  apply sig_function_translated.
  constructor; auto. constructor; auto.
  (* Stailcall *)
  exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
  exploit sel_expr_correct; eauto. intros [vf' [A B]].
  exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
  left; econstructor; split.
  exploit classify_call_correct; eauto.
  destruct (classify_call ge a) as [ | id]; intros.
  econstructor; eauto. econstructor; eauto. eapply functions_translated; eauto. apply sig_function_translated.
  destruct H2 as [b [U V]].
  econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. eapply functions_translated; eauto. subst vf; auto. apply sig_function_translated.
  constructor; auto. apply call_cont_commut; auto.
  (* Sbuiltin *)
  exploit sel_exprlist_correct; eauto. intros [vargs' [P Q]].
  exploit (external_call_mem_extends ef); eauto.
  intros [vres' [m2 [A [B [C D]]]]].
  left; econstructor; split.
  econstructor. eauto. eapply external_call_symbols_preserved; eauto.
  exact symbols_preserved. exact varinfo_preserved.
  constructor; auto.
  destruct optid; simpl; auto. apply set_var_lessdef; auto.
  (* Seq *)
  left; econstructor; split. constructor. constructor; auto. constructor; auto.
  (* Sifthenelse *)
  exploit sel_expr_correct; eauto. intros [v' [A B]].
  assert (Val.bool_of_val v' b). inv B. auto. inv H0.
  exploit eval_condition_of_expr; eauto.
  destruct (condition_of_expr (sel_expr a)) as [cond args].
  intros [vl' [C D]].
  left; exists (State (sel_function ge f) (if b then sel_stmt ge s1 else sel_stmt ge s2) k' sp e' m'); split.
  econstructor; eauto.
  constructor; auto. destruct b; auto.
  (* Sloop *)
  left; econstructor; split. constructor. constructor; auto. constructor; auto.
  (* Sblock *)
  left; econstructor; split. constructor. constructor; auto. constructor; auto.
  (* Sexit seq *)
  inv H7. left; econstructor; split. constructor. constructor; auto.
  (* Sexit0 block *)
  inv H7. left; econstructor; split. constructor. constructor; auto.
  (* SexitS block *)
  inv H7. left; econstructor; split. constructor. constructor; auto.
  (* Sswitch *)
  exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B.
  left; econstructor; split. econstructor; eauto. constructor; auto.
  (* Sreturn None *)
  exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
  left; econstructor; split.
  econstructor. simpl; eauto.
  constructor; auto. apply call_cont_commut; auto.
  (* Sreturn Some *)
  exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
  exploit sel_expr_correct; eauto. intros [v' [A B]].
  left; econstructor; split.
  econstructor; eauto.
  constructor; auto. apply call_cont_commut; auto.
  (* Slabel *)
  left; econstructor; split. constructor. constructor; auto.
  (* Sgoto *)
  exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)).
    apply call_cont_commut; eauto.
  rewrite H.
  destruct (find_label lbl (sel_stmt ge (Cminor.fn_body f)) (call_cont k'0))
  as [[s'' k'']|] eqn:?; intros; try contradiction.
  destruct H0.
  left; econstructor; split.
  econstructor; eauto.
  constructor; auto.
  (* internal function *)
  exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
  intros [m2' [A B]].
  left; econstructor; split.
  econstructor; eauto.
  constructor; auto. apply set_locals_lessdef. apply set_params_lessdef; auto.
  (* external call *)
  exploit external_call_mem_extends; eauto.
  intros [vres' [m2 [A [B [C D]]]]].
  left; econstructor; split.
  econstructor. eapply external_call_symbols_preserved; eauto.
  exact symbols_preserved. exact varinfo_preserved.
  constructor; auto.
  (* return *)
  inv H2.
  left; econstructor; split.
  econstructor.
  constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto.
Qed.

Lemma sel_initial_states:
  forall S, Cminor.initial_state prog S ->
  exists R, initial_state tprog R /\ match_states S R.
Proof.
  induction 1.
  econstructor; split.
  econstructor.
  apply Genv.init_mem_transf; eauto.
  simpl. fold tge. rewrite symbols_preserved. eexact H0.
  apply function_ptr_translated. eauto.
  rewrite <- H2. apply sig_function_translated; auto.
  constructor; auto. constructor. apply Mem.extends_refl.
Qed.

Lemma sel_final_states:
  forall S R r,
  match_states S R -> Cminor.final_state S r -> final_state R r.
Proof.
  intros. inv H0. inv H. inv H3. inv H5. constructor.
Qed.

Theorem transf_program_correct:
  forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog).
Proof.
  eapply forward_simulation_opt.
  eexact symbols_preserved.
  eexact sel_initial_states.
  eexact sel_final_states.
  eexact sel_step_correct.
Qed.

End PRESERVATION.

End WITHMEM.

author: jeremie-koenig

repo: compcert


text:
Require Import PolSBase.
Require Import PolAuxList.
Require Import PolAux.
Require Import NAux.
Require Export ArithRing.

Open Scope nat_scope.

Definition Nconvert_back (e : PExpr Z) (l : list N) : N :=
   convert_back Z N 0%N Nplus Nminus Nmult Nopp Z.abs_N l e.

Definition Nsimpl_minus (e : PExpr Z) :=
   simpl_minus
    Z Zplus Zmult Z.opp Z0 1%Z is_Z1 is_Z0 is_Zpos is_Zdiv Z.div e.

Definition Nsimpl (e : PExpr Z) :=
   simpl
    Z Zplus Zmult Z.opp Z0 1%Z is_Z1 is_Z0 is_Zpos is_Zdiv Z.div e.

Ltac
Ns term1 term2 :=
let term := constr:(Nminus term1 term2) in
let rfv := FV NCst Nplus Nmult Nminus Nopp term (@nil N) in
let fv := Trev rfv in
let expr1 := mkPolexpr Z NCst Nplus Nmult Nminus Nopp term1 fv in
let expr2 := mkPolexpr Z NCst Nplus Nmult Nminus Nopp term2 fv in
let re := eval vm_compute in (Nsimpl_minus (PEsub expr1 expr2)) in
let expr3 := match re with (PEsub ?X1 _) => X1 end in
let expr4 := match re with (PEsub _ ?X1 ) => X1 end in
let re1 := eval vm_compute in (Nsimpl (PEsub expr1 expr3)) in
let
 re1' :=
  eval
     unfold
      Nconvert_back, convert_back,  PolAuxList.pos_nth,  PolAuxList.jump,
         PolAuxList.hd,  PolAuxList.tl in (Nconvert_back (PEadd re1 expr3) fv) in
let re1'' := eval lazy beta in re1' in
let re1''' := clean_zabs_N re1'' in
let
 re2' :=
  eval
     unfold
      Nconvert_back, convert_back,  PolAuxList.pos_nth,  PolAuxList.jump,
         PolAuxList.hd,  PolAuxList.tl in (Nconvert_back (PEadd re1 expr4) fv) in
let re2'' := eval lazy beta in re2' in
let re2''' := clean_zabs_N re2'' in
replace2_tac term1 term2 re1''' re2'''; [idtac | ring | ring].
(*
(replace term with re2; [idtac | try ring]).
*)

Ltac
Npols :=
match goal with
| |- (?X1 = ?X2)%N =>
Ns X1 X2; apply Nplus_eq_compat_l
| |- (?X1 <> ?X2)%N =>
Ns X1 X2; apply Nplus_neg_compat_l
| |- (?X1 < ?X2)%N =>
Ns X1 X2; apply Nplus_lt_compat_l
| |- (?X1 > ?X2)%N =>
Ns X1 X2; apply Nplus_gt_compat_l
| |- (?X1 <= ?X2)%N =>
Ns X1 X2; apply Nplus_le_compat_l
| |- (?X1 >= ?X2)%N =>
Ns X1 X2; apply Nplus_ge_compat_l
| _ => fail end.

Ltac
hyp_Npols H :=
generalize H;
let tmp := fresh "tmp" in
match (type of H) with
   (?X1 = ?X2)%N =>
Ns X1 X2; intros tmp; generalize (Nplus_reg_l _ _ _ tmp); clear H tmp; intro H
|  (?X1 <> ?X2)%N =>
Ns X1 X2; intros tmp; generalize (Nplus_neg_reg_l _ _ _ tmp); clear H tmp; intro H
|  (?X1 < ?X2)%N =>
Ns X1 X2; intros tmp; generalize (Nplus_lt_reg_l _ _ _ tmp); clear H tmp; intro H
|  (?X1 > ?X2)%N =>
Ns X1 X2; intros tmp; generalize (Nplus_gt_reg_l _ _ _ tmp); clear H tmp; intro H
|  (?X1 <= ?X2)%N =>
Ns X1 X2; intros tmp; generalize (Nplus_le_reg_l _ _ _ tmp); clear H tmp; intro H
|  (?X1 >= ?X2)%N =>
Ns X1 X2; intros tmp; generalize (Nplus_ge_reg_l _ _ _ tmp); clear H tmp; intro H
| _ => fail end.

author: UCSD-PL


text:
Require Export Basics.

Require Export EnvListAux7.
Require Export EnvListAuxT1.

Require Export Coq.Program.Equality.
Require Import Coq.Init.Specif.
Require Import Coq.Arith.PeanoNat.
Require Import Omega.
Require Import Coq.Lists.List.

Require Import TPipStaticM2.
Require Import TPipDynamicM2.
Require Import TRInductM2.
Require Import WeakM2.
Require Import IdModType.

Module TSoundness (IdT: IdModType) <: IdModType.
(* Export IdT. *)

Definition Id := IdT.Id.
Definition IdEqDec := IdT.IdEqDec.
Definition IdEq := IdT.IdEq.
Definition W := IdT.W.
Definition Loc_PI := IdT.Loc_PI.
Definition BInit := IdT.BInit.
Definition WP := IdT.WP.

Module WeakeningC := Weakening IdT.
Export WeakeningC.

Definition SoundExpA (fenv: funEnv) (env: valEnv)
                     (e: Exp) (t: VTyp) (n: W)
  := sigT2 (fun v: Value => ValueTyping v t)
           (fun v: Value => sigT (fun n': W =>
                         EClosure fenv env (Conf Exp n e)
                                                (Conf Exp n' (Val v)))).

Definition Par_F := fun (f: Fun) (ft: FTyp)
                         (k: FunTyping f ft) =>
    forall (fps: valTC) (t: VTyp),
    ft = FT fps t ->
    forall (i: nat) (fenv': funEnv)
           (x: Id) (e0 e1: Exp),
       f = FC fenv' fps e0 e1 x i ->
       forall (n: W) (env: valEnv),
       EnvTyping env fps ->
       match i with
         | 0 => SoundExpA fenv' env e0 t n
         | S j => SoundExpA (updateE fenv' x (FC fenv' fps e0 e1 x j))
                           env e1 t n
       end.

Definition Par_F_Mod := fun (f: Fun) (ft: FTyp)
                         (k: FunTyping f ft) =>
    forall env: valEnv,
       EnvTyping env (extParType ft) ->
    forall n: W,
    forall (fenv': funEnv) (e0 e1: Exp)
           (x: Id) (i: nat),
      let fps := extParType ft in
      let t := extRetType ft in
       f = FC fenv' fps e0 e1 x i ->
       match i with
         | 0 => SoundExpA fenv' env e0 t n
         | S j => SoundExpA (updateE fenv' x (FC fenv' fps e0 e1 x j))
                           env e1 t n
       end.

Definition Par_Q := fun (ftenv: funTC) (fenv: funEnv)
                         (q: QFun) (ft: FTyp)
                         (k: QFunTyping ftenv fenv q ft) =>
   FEnvTyping fenv ftenv ->
   forall n: W,
     sigT2 (fun f: Fun =>
                  sigT (fun k1: FunTyping f ft => Par_F f ft k1))
           (fun f: Fun => QFClosure fenv (Conf QFun n q)
                                           (Conf QFun n (QF f))).

Definition Par_E :=
     fun (ftenv: funTC) (tenv: valTC) (fenv: funEnv)
                        (e: Exp) (t: VTyp)
                        (k: ExpTyping ftenv tenv fenv e t) =>
  FEnvTyping fenv ftenv ->
  forall env: valEnv,
  EnvTyping env tenv ->
  forall n: W, SoundExpA fenv env e t n.

Definition Par_P :=
      fun (ftenv: funTC) (tenv: valTC) (fenv: funEnv)
                         (ps: Prms) (pt: PTyp)
                         (k: PrmsTyping ftenv tenv fenv ps pt) =>
  FEnvTyping fenv ftenv ->
  forall env: valEnv,
  EnvTyping env tenv ->
  forall n: W,
      sigT (fun es: list Exp =>
        sigT2 (isValueList2T es)
              (fun vs: list Value =>
                 prod (PrmsTyping emptyE emptyE emptyE (PS es) pt)
                      (sigT (fun n': W =>
                         PrmsClosure fenv env (Conf Prms n ps)
                                                   (Conf Prms n' (PS es)))))).

Definition ExpTypingSoundA_rect :=
  ExpTyping_str_rect
           Par_F Par_Q Par_E Par_P.

Lemma WellTypedEvalM :
  forall (ftenv: funTC) (tenv: valTC) (fenv: funEnv)
   (e: Exp) (t: VTyp),
      ExpTyping ftenv tenv fenv e t ->
      FEnvTyping fenv ftenv ->
      forall env: valEnv,
      EnvTyping env tenv ->
      forall n: W, SoundExpA fenv env e t n.

Proof.
eapply ExpTypingSoundA_rect.

- (** base Par_SSL *)
  unfold Par_SSL, Par_E.
  constructor.

- (** step Par_SSL *)
  unfold Par_SSL, Par_E.
  intros.
  constructor.
  + assumption.
  + assumption.
  + assumption.

- (** base Par_SSA *)
  unfold Par_SSA, Par_F.
  constructor.

- (** step Par_SSA *)
  unfold Par_SSA, Par_F.
  intros.
  constructor.
  + assumption.
  + assumption.
  + assumption.

- (** Par_SSB *)
  unfold Par_SSB, Par_SSA, Par_F.
  intros.
  eapply (Forall2BT_split FunTyping _ _
                         fenv fenv0 fenv1 ftenv ftenv0 ftenv1 x f t).
  + assumption.
  + assumption.
  + assumption.
  + assumption.
  + assumption.
  + assumption.
  + assumption.
  + assumption.

- (** base Par_F *)
  unfold Par_F, Par_E.
  intros.
  inversion H; subst.
  inversion H0; subst.
  specialize (X m env X0 n).
  assumption.

- (** step Par_F *)
  unfold Par_F, Par_E.
  intros.
  inversion H; subst.
  inversion H0; subst.
  rename n into i.
  rename fenv'0 into fenv.
  eapply updateFEnvLemma with (x:= x0)
              (v1:= FC fenv fps e2 e3 x0 i) (v2:= FT fps t0) in m.
  specialize (X m env X1 n0).
  assumption.
  assumption.

- (** Par_Q - QF *)
  unfold Par_Q, Par_F.
  intros.
  constructor 1 with (x:=f).
  * constructor.
    assumption.
    assumption.
  * constructor.

- (** Par_Q - FId *)
  unfold Par_Q, Par_SSB, Par_F, Par_SSA.
  intros.
  inversion X; subst.
  clear X.
  constructor 1 with (x:=f).
  + constructor.
    assumption.
    assumption.
  + constructor.
    constructor.
    constructor.
    clear X1 X2 X3.
    inversion m; subst.
    rewrite H0.
    eapply ExRelValTNone with (venv:=ls1) in H.
    * eapply findEexApp with (env:=(x,f)::ls3) in H.
      rewrite <- H at 1.
      simpl.
      destruct (IdT.IdEqDec x x).
      {- auto. }
      {- intuition n0. }
    * auto.
    * eauto.
(** Par_E *)
-  (* modify *)
  unfold Par_E, SoundExpA.
  intros ftenv tenv fenv T1 T2 VT1 VT2 XF q H H0 env H0' n.
  inversion H; subst.
  destruct v.
  destruct v.
  inversion H1; subst.
  subst T.
  simpl in H2.
  destruct H2.
  constructor 1 with (x:=cst T2 (b_eval _ _ XF n v)).
  + constructor.
    * reflexivity.
    * constructor.
  + inversion H; subst.
    * inversion H1; subst.
      subst T.
      simpl in H2.
      clear H2.
      constructor 1 with (x:=b_exec _ _ XF n v).
      eapply StepIsEClos.
      constructor.
  + inversion X; subst.
    eapply ExTDefNatT with (venv:=env) (T:=T1) in X0.
    * destruct X0 as [v k].
      constructor 1 with (x:= cst T2 (b_eval _ _ XF n v)).
      econstructor.
      {- constructor. }
      {- econstructor. }
      {- constructor 1 with (x:=b_exec _ _ XF n v).
         econstructor.
         econstructor.
         econstructor.
         eassumption.
         eapply StepIsEClos.
         constructor. }
    * assumption.
    * assumption.
    * reflexivity.
- (* return *)
  unfold Par_E, SoundExpA.
  intros G ftenv tenv fenv q t H H0 env H0' n.
  inversion H; subst.
  + constructor 1 with (x:=v).
    * assumption.
    * constructor 1 with (x:=n).
      econstructor.
      {- econstructor. }
      {- constructor. }
  + inversion X; subst.
    eapply ExTDefVal with (venv:=env) in X0.
    * destruct X0 as [v k1 k2].
      constructor 1 with (x:=v).
      {- assumption. }
      {- constructor 1 with (x:=n).
         econstructor.
         + constructor.
           constructor.
           eassumption.
         + eapply StepIsEClos.
           constructor.
      }
    * auto.
- (* bindN *)
  unfold Par_E, SoundExpA.
  intros ftenv tenv fenv e1 e2 t1 t2.
  intros k1 k2 IH1 IH2.
  intros H0 env H0' n.
  specialize (IH1 H0 env H0' n).
  destruct IH1 as [v0 k3 H2].
  destruct H2 as [n0 H2].
  specialize (IH2 H0 env H0' n0).
  destruct IH2 as [v2 k4 H3].
  destruct H3 as [n2 H3].
  constructor 1 with (x:=v2).
  + auto.
  + constructor 1 with (x:=n2).
    eapply (EClosConcat fenv env).
    * instantiate  (1 := Conf Exp n0 (BindN (Val v0) e2)).
      apply  BindN_extended_congruence.
      assumption.
    * econstructor.
      {- econstructor. }
      {- assumption. }
- (* BindS *)
  unfold Par_E, SoundExpA.
  intros ftenv tenv tenv' fenv x e1 e2 t1 t2.
  intros H k1 k2 IH1 IH2.
  intros H0 env H0' n.
  specialize (IH1 H0 env H0' n).
  destruct IH1 as [v1 k3 H1].
  destruct H1 as [n0 H1].
  specialize (IH2 H0 (updateE env x v1)).
  cut (EnvTyping (updateE env x v1) (updateE tenv x t1)).
  + intro.
    rewrite H in IH2.
    specialize (IH2 X n0).
    destruct IH2 as [v2 k4 H2].
    destruct H2 as [n1 H2].
    constructor 1 with (x:=v2).
    * assumption.
    * constructor 1 with (x:=n1).
      eapply EClosConcat.
      {- instantiate (1:= (Conf Exp n0 (BindS x (Val v1) e2))).
         apply BindS_extended_congruence.
         assumption.
      }
      {- eapply EClosConcat.
         + eapply StepIsEClos.
           econstructor.
         + eapply EClosConcat.
           * eapply BindMS_extended_congruence.
             {- reflexivity. }
             {- reflexivity. }
             {- unfold overrideE.
                rewrite app_nil_l.
                eassumption.
             }
           * eapply StepIsEClos.
             constructor.
       }
  + apply updateVEnvLemma.
    * assumption.
    * assumption.
- (* BindMS *)
  unfold Par_E, SoundExpA.
  intros ftenv ftenvP ftenv' tenv tenvP tenv' fenv fenvP fenv' envP e t.
  intros k1 k2 k3 E1 E2 E3 k4 IH.
  intros H0 env H0' n.
  eapply (overrideVEnvLemma envP env tenvP tenv k1) in H0'.
  eapply (overrideFEnvLemma fenvP fenv ftenvP ftenv k3) in H0.
  cut (FEnvTyping fenv' ftenv').
  + cut (EnvTyping (overrideE envP env) tenv').
    * intros H1' H1.
      specialize (IH H1 (overrideE envP env) H1' n).
      destruct IH as [v k5 H2].
      destruct H2 as [n1 H2].
      constructor 1 with (x:=v).
      {- auto. }
      {- constructor 1 with (x:=n1).
         eapply (EClosConcat fenv env).
         + eapply BindMS_extended_congruence.
           * reflexivity.
           * reflexivity.
           * rewrite <- E3.
             eassumption.
         + eapply StepIsEClos.
           constructor.
      }
    * rewrite E1.
      assumption.
  + rewrite E2.
    rewrite E3.
    assumption.
- (* Apply *)
  unfold Par_Q, Par_P, Par_E, SoundExpA.
  intros ftenv tenv fps fenv q ps pt t.
  intros E1 k1 k2 k3 IH1 IH2.
  intros H0 env H0' n.

  cut (sigT (fun n' : W =>
        (sigT (fun f: Fun =>
          sigT2 (fun es: list Exp => isValueListT es)
             (fun es: list Exp => prod
               (EClosure fenv env (Conf Exp n (Apply q ps))
                         (Conf Exp n' (Apply (QF f) (PS es))))
               (sigT2 (fun v : Value =>
                    sigT (fun n'' : W =>
                       EClosure fenv env
                             (Conf Exp n' (Apply (QF f) (PS es)))
                             (Conf Exp n'' (Val v))))
                    (fun v: Value => ValueTyping v t))))))).

  intros.
  + destruct X as [n1 X].
    destruct X as [f X].
    destruct X as [vls k4 X].
    destruct X as [H1 X].
    destruct X as [v X k5].
    destruct X as [n2 H2].
    constructor 1 with (x:=v).
    * assumption.
    * constructor 1 with (x:=n2).
      eapply EClosConcat.
      {- eassumption. }
      {- eassumption. }
  + specialize (IH1 H0 n).
    destruct IH1 as [f H3 H1].
    destruct H3 as [k5 HF].
    (* destruct H1 as [n1 H1]. *)
    specialize (IH2 H0 env H0' n).
    destruct IH2 as [es H2].
    destruct H2 as [vs k6 H2].
    destruct H2 as [k7 H2].
    destruct H2 as [n1 H2].
    constructor 1 with (x:=n1).
    constructor 1 with (x:=f).
    constructor 1 with (x:=es).
    * eapply isValueList2IsValueT.
      eassumption.
    * destruct pt.
      inversion E1; subst.
      split.
      {- eapply EClosConcat.
         + instantiate (1:=(Conf Exp n (Apply (QF f) ps))).
           eapply Apply2_extended_congruence.
           assumption.
         + eapply Apply1_extended_congruence.
           assumption.
      }
      {- eapply matchListsAux02_T with (vs:=vs) in k7.
         assert (length fps = length vs) as H5.
         + eapply prmsAux2.
           * eassumption.
         + unfold Par_F in HF.
           specialize (HF fps t eq_refl).
           eapply prmsTypingAux_T in k7.
           inversion k5; subst.
           * specialize (HF 0 fenv0 x e0 e1 eq_refl).
             specialize (HF n1 (mkVEnv fps vs)).
             {- specialize (HF k7).
                destruct HF as [v k8 HF].
                destruct HF as [n2 HF].
                constructor 1 with (x:=v).
                + constructor 1 with (x:=n2).
                  econstructor.
                  * eapply Apply_EStep0.
                    {- eassumption. }
                    {- assumption. }
                    {- reflexivity. }
                  * eapply EClosConcat.
                    {- eapply BindMS_extended_congruence.
                       + reflexivity.
                       + reflexivity.
                       + eapply (weak fenv0 fenv (mkVEnv fps vs) env)
                                in HF.
                         eassumption.
                    }
                    {- apply StepIsEClos.
                       constructor.
                    }
                + assumption.
             }
           * specialize (HF (S n0) fenv0 x e0 e1 eq_refl).
             specialize (HF n1 (mkVEnv fps vs)).
             {- specialize (HF k7).
                destruct HF as [v k8 HF].
                destruct HF as [n2 HF].
                constructor 1 with (x:=v).
                + constructor 1 with (x:=n2).
                  econstructor.
                  * eapply Apply_EStep1.
                    {- eassumption. }
                    {- assumption. }
                    {- reflexivity. }
                  * eapply EClosConcat.
                    {- eapply BindMS_extended_congruence.
                       + reflexivity.
                       + reflexivity.
                       + eapply weak.
                         eassumption.
                    }
                    {- apply StepIsEClos.
                       constructor.
                    }
                + assumption.
             }
          * assumption.
        + assumption.
      }
- (* Val *)
  unfold Par_E, SoundExpA.
  intros.
  constructor 1 with (x:=v).
  + assumption.
  + constructor 1 with (x:=n).
    constructor.
- (* IFThenElse *)
  unfold Par_E, SoundExpA.
  intros.
  specialize (X X2 env X3 n).
  destruct X as [v K X].
  destruct X as [n' X].
  specialize (X0 X2 env X3 n').
  destruct X0 as [v0 K0 X0].
  destruct X0 as [n0 X0].
  specialize (X1 X2 env X3 n').
  destruct X1 as [v1 K1 X1].
  destruct X1 as [n1 X1].
  inversion K; subst.
  subst T.
  destruct v as [T v].
  destruct v.

  unfold Bool in H.
  unfold vtyp in H.
  simpl in H.
  inversion H; subst.

  destruct v.
  + constructor 1 with (x:=v0).
    assumption.
    constructor 1 with (x:=n0).
    eapply EClosConcat.
    instantiate (1:=Conf Exp n'
       (IfThenElse (Val (existT ValueI bool (Cst bool true))) e2 e3)).
    eapply IfThenElse_extended_congruence.
    eassumption.

    econstructor.
    econstructor.

    eassumption.
(*
    eapply IfThenElse_extended_congruence.
    exact X.
    econstructor.
    constructor.
    assumption.
*)
  + constructor 1 with (x:=v1).
    assumption.
    constructor 1 with (x:=n1).
    eapply EClosConcat.
    eapply IfThenElse_extended_congruence.
    eassumption.
    econstructor.
    econstructor.
    eassumption.
- (** Par_P *)
  unfold Par_SSL, Par_E, Par_P, SoundExpA.
  intros.
  dependent induction X.
  constructor 1 with (x:=nil).
  constructor 1 with (x:=nil).
  constructor.
  simpl.
  auto.
  split.
  constructor.
  constructor.
  constructor 1 with (x:=n).
  constructor.
  (**)
  clear X.
  specialize (p0 X0 env X1 n).
  destruct p0 as [v k1 X2].
  destruct X2 as [n1 H].
  inversion m; subst.
  specialize (IHX X2).
  specialize (IHX X0 env X1 n1).
  destruct IHX as [es IHX].
  destruct IHX as [vs k2 IHX].
  destruct IHX as [k3 IHX].
  destruct IHX as [n2 k4].
  constructor 1 with (x:=(Val v::es)).
  constructor 1 with (x:=v::vs).
  constructor.
  eapply IsValueList2T.
  simpl.
  inversion k2; subst.
  auto.
  split.
  constructor.
  constructor.
  constructor.
  assumption.
  inversion k3; subst.
  assumption.
  constructor 1 with (x:=n2).
  eapply PrmsConcat.
  eapply Pars_extended_congruence2.
  eassumption.
  eapply Pars_extended_congruence1.
  assumption.
Defined.

End TSoundness.

author: CherifSami