Finished proof that C program correctly implements cholesky_jik

C/verif_cholesky.v

@@ -35,16 +35,16 @@ Definition sum_upto (n: Z) (f: Z -> ftype t) :=
 
 Definition cholesky_jik_ij (n: Z) (A R: Z -> Z -> ftype t) (i j: Z) : Prop :=
  (0 <= j < n) ->
- (0 <= i < j -> R i j = BDIV (subtract_loop A R i j j) (R i i))
- /\ (i=j -> R i j = BSQRT _ _ (subtract_loop A R i j j)).
+ (0 <= i < j -> R i j = BDIV (subtract_loop A R i j i) (R i i))
+ /\ (i=j -> R i j = BSQRT _ _ (subtract_loop A R i j i)).
 
 
 Definition cholesky_jik_spec (n: Z) (A R: Z -> Z -> ftype t) : Prop :=
  forall i j, cholesky_jik_ij n A R i j.
 
 Definition cholesky_jik_upto (n imax jmax : Z) (A R : Z -> Z -> ftype t) : Prop :=
  forall i j, 
- (j<jmax -> forall i, cholesky_jik_ij n A R i j)
+ (j<jmax -> cholesky_jik_ij n A R i j)
  /\ (j=jmax -> i<imax -> cholesky_jik_ij n A R i j).
 
 Definition done_to_ij (n i j: Z) (R: Z -> Z -> ftype Tdouble) (i' j': Z) : val :=
@@ -119,6 +119,13 @@ Proof.
 intros. revert lo; induction n; simpl; intros; auto.
 rewrite Zlength_cons, IHn. lia.
 Qed.
+
+
+Lemma length_iota:
+ forall lo n, length (iota lo n) = n.
+Proof.
+intros. revert lo; induction n; simpl; intros; auto.
+Qed.
 
 
 
@@ -161,6 +168,32 @@ Definition updij {T} (R: Z -> Z -> T) i j x :=
  fun i' j' => if zeq i i' then if zeq j j' then x else R i' j' else R i' j'.
 
 
+Lemma upto_iota:
+ forall n, upto n= map Z.of_nat (iota O n).
+Proof.
+intros.
+transitivity (map (Z.add (Z.of_nat O)) (upto n)).
+induction n; simpl; f_equal. rewrite map_map. f_equal.
+forget O as x. revert x; induction n; simpl; intros; f_equal.
+lia. rewrite <- (IHn (S x)). rewrite map_map. f_equal. extensionality y. lia.
+Qed.
+
+
+Lemma iota_range: forall k n, In k (iota 0 n) -> (k<n)%nat.
+Proof.
+intros.
+replace k with (k-O)%nat by lia.
+forget O as u.
+revert k u H; induction n; intros; try lia.
+contradiction H.
+replace (S n) with (n+1)%nat in H by lia.
+rewrite iota_plus1 in H.
+rewrite in_app in H. destruct H.
+apply IHn in H; lia.
+destruct H; try contradiction. lia.
+Qed.
+
+
 Lemma upd_Znth_lists_of_fun:
  forall d N n R i j x,
  0 <= i <= j -> j < N ->
@@ -176,15 +209,177 @@ set (f i0 := list_of_fun _ _).
 rewrite Znth_map by (rewrite Zlength_iota; lia).
 rewrite Znth_i_iota by lia.
 simpl.
-Admitted.
+rewrite upd_Znth_eq by (rewrite Zlength_map, Zlength_iota; lia).
+rewrite map_length, length_iota.
+rewrite upto_iota.
+rewrite map_map.
+apply map_ext_in.
+intro k.
+intro.
+apply iota_range in H1.
+subst f.
+if_tac.
+- subst i.
+unfold list_of_fun.
+rewrite upd_Znth_eq by (rewrite Zlength_map, Zlength_iota; lia).
+rewrite map_length.
+rewrite length_iota.
+rewrite upto_iota, map_map.
+apply map_ext_in.
+intros.
+apply iota_range in H2.
+if_tac.
++
+subst j.
+unfold done_to_ij.
+rewrite !if_false by lia.
+unfold updij.
+rewrite !if_true by lia.
+reflexivity.
++
+rewrite Znth_map by (rewrite Zlength_iota; lia).
+unfold done_to_ij.
+rewrite Nat2Z.id.
+unfold updij.
+rewrite !if_false by lia.
+rewrite Znth_i_iota by lia.
+rewrite Nat2Z.id.
+simpl.
+if_tac.
+rewrite !if_false by lia. auto.
+if_tac.
+rewrite !if_false by lia.
+rewrite !if_true by lia.
+rewrite if_false by lia.
+auto.
+if_tac; try lia.
+rewrite !if_false by lia.
+auto. 
+-
+rewrite Znth_map by (rewrite Zlength_iota; lia).
+rewrite Znth_i_iota by lia.
+simpl Nat.add.
+rewrite Nat2Z.id.
+f_equal.
+unfold done_to_ij.
+simpl.
+extensionality j'.
+rewrite !if_false by lia.
+if_tac.
+if_tac; auto.
+if_tac.
+if_tac; auto.
+if_tac.
+rewrite if_false by lia.
+unfold updij.
+rewrite if_false by lia.
+auto.
+if_tac; try lia.
+if_tac; try lia.
+rewrite if_false by lia.
+rewrite if_true by lia.
+unfold updij.
+rewrite if_false by lia.
+auto.
+rewrite if_false by lia.
+rewrite if_false by lia.
+auto.
+if_tac; auto.
+Qed.
+
 
 Lemma update_i_lt_j:
  forall {t: type} {STD: is_standard t} n i j (A R: Z -> Z -> ftype t),
  0 <= i < j -> j < n ->
  cholesky_jik_upto n i j A R ->
  let rij := BDIV (subtract_loop A R i j i) (R i i) in
  cholesky_jik_upto n (i + 1) j A (updij R i j rij).
-Admitted.
+Proof.
+intros.
+intros i' j'.
+subst rij.
+split; intros.
+-
+specialize (H1 i' j').
+destruct H1 as [H1 _]. specialize (H1 H2).
+split; intros.
++
+specialize (H1 H3). clear H3.
+destruct H1 as [? _]. specialize (H1 H4). 
+unfold updij.
+destruct (zeq j j'); try lia.
+if_tac; try lia.
+* rewrite if_false by lia.
+ subst i. rewrite H1. f_equal.
+ unfold subtract_loop.
+ f_equal. rewrite !map_map.
+ apply map_ext_in.
+ intros. apply iota_range in H3.
+ f_equal.
+ if_tac; try lia; auto.
+ rewrite if_false by lia. auto.
+* rewrite H1. f_equal.
+ unfold subtract_loop.
+ f_equal. rewrite !map_map.
+ apply map_ext_in.
+ intros. apply iota_range in H5.
+ f_equal.
+ if_tac; try lia; auto.
+ rewrite if_false by lia. auto.
+ if_tac; auto. if_tac; try lia. auto.
++ specialize (H1 H3).
+ destruct H1 as [_ H1].
+ unfold updij. subst i'.
+ if_tac; try lia.
+ * rewrite if_false by lia.
+ specialize (H1 (eq_refl _)).
+ rewrite H1. f_equal.
+ unfold subtract_loop.
+ f_equal. rewrite !map_map.
+ apply map_ext_in.
+ intros. apply iota_range in H5.
+ f_equal.
+ if_tac; try lia; auto.
+ rewrite if_false by lia. auto.
+ *
+ rewrite H1 by lia. f_equal.
+ unfold subtract_loop.
+ f_equal. rewrite !map_map.
+ apply map_ext_in.
+ intros. apply iota_range in H5.
+ f_equal.
+ if_tac; try lia; auto.
+ rewrite if_false by lia. auto.
+ if_tac; try lia; auto. if_tac; auto; try lia.
+-
+ red in H1|-*.
+ subst j'.
+ intro.
+ split; intros; [ | lia].
+ + unfold updij. destruct (zeq j j); try lia. clear e.
+ destruct (zeq j i'); try lia.
+ replace (if zeq i i' then R i' i' else R i' i') with (R i' i') by (if_tac; auto).
+ if_tac.
+ * subst i'. clear n0 H3 H0 H4.
+ f_equal.
+ match goal with |- _ = _ _ ?ff _ _ _ => set (f:=ff) end.
+ unfold subtract_loop.
+ f_equal. rewrite !map_map.
+ apply map_ext_in.
+ intros. apply iota_range in H0.
+ subst f. simpl. if_tac; try lia; auto.
+ * assert (i'<i) by lia. clear H5 H3 n0.
+ specialize (H1 i' j). destruct H1 as [_ H1].
+ destruct H1 as [H1 _]; try lia. rewrite H1 by auto.
+ f_equal.
+ unfold subtract_loop.
+ f_equal. rewrite !map_map.
+ apply map_ext_in.
+ intros. apply iota_range in H3.
+ f_equal.
+ if_tac; try lia; auto.
+ rewrite if_false by lia. auto.
+Qed.
 
 Lemma subtract_another:
  forall
@@ -369,7 +564,8 @@ forward_for_simple_bound j
  intros i' j'.
  destruct (zlt j' (j+1));
  [ | split; intros; [ lia | split; intros; lia]].
- assert (Hsub: forall i j', 0 <= i <= j' -> j'<=j -> subtract_loop A R' i j' j' = subtract_loop A R i j' j'). {
+ assert (Hsub: forall i j', 0 <= i <= j' -> i'<=j'<=j -> 
+ subtract_loop A R' i j' i' = subtract_loop A R i j' i'). {
  clear j' l; intros i j' Hi Hj'.
  set (x := BSQRT _ _ _) in R'. clearbody x.
  subst R'. destruct H0.
@@ -378,34 +574,34 @@ forward_for_simple_bound j
  rewrite !map_map.
  pose (f z := BMULT z z ).
  set (g1 := BMULT). set (g2 := BMINUS).
- set (a := A i j'). clearbody a.
+ set (a := A i j'). clearbody a. clearbody g1. clearbody g2.
  set (n:=j) at 1 2 3 4.
- set (u := O). assert (Z.of_nat (u+ Z.to_nat j')<=n) by lia. clearbody u. clearbody n.
- revert a u H; induction (Z.to_nat j'); intros; auto.
+ set (u := O). assert (Z.of_nat (u+ Z.to_nat i')<=n) by lia. clearbody u. clearbody n.
+ revert a u H; induction (Z.to_nat i'); intros; auto.
  simpl. rewrite IHn0 by lia. f_equal. f_equal. f_equal. unfold updij.
  rewrite if_false by lia. auto. unfold updij. rewrite if_false by lia. auto.
  }
  destruct (zlt j' j); split; intros; try lia.
- ++ clear H2 i' l.
- destruct (H1 i j') as [? _].
- specialize (H2 l0 i).
+ ++ clear H2 l.
+ destruct (H1 i' j') as [? _].
+ specialize (H2 l0).
  set (x := BSQRT _ _ _) in R'. clearbody x. clear - Hsub H2 l0 H0.
  intro. specialize (H2 H). destruct H2.
  split; intros.
  ** rewrite Hsub by lia.
  unfold R', updij. rewrite !if_false by lia. auto. 
  ** rewrite Hsub by lia. 
  unfold R', updij. rewrite !if_false by lia. auto. 
- ++ assert (j'=j) by lia. subst j'. clear l g H2 i'.
+ ++ assert (j'=j) by lia. subst j'. clear l g H2.
  red in H1.
  split; intros.
  **
- destruct (H1 i j) as [_ ?]. specialize (H4 (eq_refl _) ltac:(lia)).
+ destruct (H1 i' j) as [_ ?]. specialize (H4 (eq_refl _) ltac:(lia)).
  red in H4. destruct H4 as [? _]; try lia.
  rewrite Hsub by lia.
  unfold R'. unfold updij. rewrite !if_false by lia.
  apply H4; auto. 
- ** subst i. rewrite Hsub by lia. unfold R', updij.
+ ** subst i'. rewrite Hsub by lia. unfold R', updij.
  rewrite !if_true by auto. auto.
  - Intros R. Exists R.
  rewrite <- N_eq in *.