From bb22511fef108219be24c5c48664d142caad1caf Mon Sep 17 00:00:00 2001 From: ZhuangYumin Date: Sat, 21 Jun 2025 08:17:32 +0000 Subject: [PATCH] only last wh ich implies left --- projects/lib/gmp_proof_manual.v | 32 ++++++++++++++++++++++++++++++-- 1 file changed, 30 insertions(+), 2 deletions(-) diff --git a/projects/lib/gmp_proof_manual.v b/projects/lib/gmp_proof_manual.v index c82e028..3b5fa6e 100644 --- a/projects/lib/gmp_proof_manual.v +++ b/projects/lib/gmp_proof_manual.v @@ -699,10 +699,38 @@ Proof. Qed. Lemma proof_of_mpn_add_1_which_implies_wit_1 : mpn_add_1_which_implies_wit_1. -Proof. Admitted. +Proof. + pre_process. + unfold mpd_store_Z_compact. + Intros l. + Exists l. + unfold mpd_store_list. + entailer!. + subst n_pre. + entailer!. +Qed. Lemma proof_of_mpn_add_1_which_implies_wit_2 : mpn_add_1_which_implies_wit_2. -Proof. Admitted. +Proof. + pre_process. + pose proof (store_uint_array_divide rp_pre cap2 l2 0). + pose proof (Zlength_nonneg l2). + specialize (H0 ltac:(lia) ltac:(lia)). + destruct H0 as [H0 _]. + simpl in H0. + entailer!. + rewrite (sublist_nil l2 0 0) in H0; [ | lia]. + sep_apply H0. + entailer!. + unfold store_uint_array, store_uint_array_rec. + unfold store_array. + rewrite (sublist_self l2 cap2); [ | lia ]. + assert (rp_pre + 0 = rp_pre). { lia. } + rewrite H2; clear H2. + assert (cap2 - 0 = cap2). { lia. } + rewrite H2; clear H2. + reflexivity. +Qed. Lemma proof_of_mpn_add_1_which_implies_wit_3 : mpn_add_1_which_implies_wit_3. Proof. Admitted. \ No newline at end of file