diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-06-26 10:08:16 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-06-26 10:08:44 +0100 |
| commit | 7eeb169b982af90fac9873956e70d2c471555c31 (patch) | |
| tree | 53a1a3a98bb5b1e38891ca77af17c10d852daea0 /src/hls/GiblePargenproofCommon.v | |
| parent | e9f748f8e302f4d9977661e9c51ddaf5410bdec6 (diff) | |
| download | vericert-7eeb169b982af90fac9873956e70d2c471555c31.tar.gz vericert-7eeb169b982af90fac9873956e70d2c471555c31.zip | |
Finish some proofs and remove unnecessary Admitted
Diffstat (limited to 'src/hls/GiblePargenproofCommon.v')
| -rw-r--r-- | src/hls/GiblePargenproofCommon.v | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v index 0a09c23..345836f 100644 --- a/src/hls/GiblePargenproofCommon.v +++ b/src/hls/GiblePargenproofCommon.v @@ -309,38 +309,38 @@ Lemma prune_predicated_mutexcl : predicated_mutexcl y. Proof. unfold prune_predicated; intros. - Admitted. -#[local] Hint Resolve prune_predicated_mutexcl : mte. + Abort. +(*#[local] Hint Resolve prune_predicated_mutexcl : mte.*) Lemma app_predicated_mutexcl : forall A p (x: predicated A) y, predicated_mutexcl x -> predicated_mutexcl y -> predicated_mutexcl (app_predicated p x y). -Proof. Admitted. -#[local] Hint Resolve app_predicated_mutexcl : mte. +Proof. Abort. +(*#[local] Hint Resolve app_predicated_mutexcl : mte.*) Lemma seq_app_predicated_mutexcl : forall A B (f: predicated (A -> B)) y, predicated_mutexcl f -> predicated_mutexcl y -> predicated_mutexcl (seq_app f y). -Proof. Admitted. -#[local] Hint Resolve seq_app_predicated_mutexcl : mte. +Proof. Abort. +(* #[local] Hint Resolve seq_app_predicated_mutexcl : mte. *) Lemma all_predicated_mutexcl: forall f l, all_mutexcl f -> predicated_mutexcl (merge (list_translation l f)). -Proof. Admitted. -#[local] Hint Resolve all_predicated_mutexcl : mte. +Proof. Abort. +(* #[local] Hint Resolve all_predicated_mutexcl : mte. *) Lemma flap2_predicated_mutexcl : forall A B C (f: predicated (A -> B -> C)) x y, predicated_mutexcl f -> predicated_mutexcl (flap2 f x y). -Proof. Admitted. -#[local] Hint Resolve flap2_predicated_mutexcl : mte. +Proof. Abort. +(* #[local] Hint Resolve flap2_predicated_mutexcl : mte. *) Lemma all_mutexcl_set : forall f n r, @@ -370,11 +370,11 @@ Lemma all_mutexcl_maintained : Proof. destruct i; cbn -[seq_app]; intros; unfold Option.bind in *; repeat destr; inv H0. - trivial. - - apply prune_predicated_mutexcl in Heqo1; auto with mte. - - apply prune_predicated_mutexcl in Heqo0; auto with mte. - - apply prune_predicated_mutexcl in Heqo0; auto with mte. - apply app_predicated_mutexcl; auto with mte. - - unfold all_mutexcl; intros; rewrite forest_pred_reg; auto. - - unfold all_mutexcl; intros. unfold "<-e". unfold "#r". cbn. - fold (get_forest x f). auto. -Qed. + (* - apply prune_predicated_mutexcl in Heqo1; auto with mte. *) + (* - apply prune_predicated_mutexcl in Heqo0; auto with mte. *) + (* - apply prune_predicated_mutexcl in Heqo0; auto with mte. *) + (* apply app_predicated_mutexcl; auto with mte. *) + (* - unfold all_mutexcl; intros; rewrite forest_pred_reg; auto. *) + (* - unfold all_mutexcl; intros. unfold "<-e". unfold "#r". cbn. *) + (* fold (get_forest x f). auto. *) +Abort. |