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/GiblePargenproofEvaluable.v | |
| parent | e9f748f8e302f4d9977661e9c51ddaf5410bdec6 (diff) | |
| download | vericert-7eeb169b982af90fac9873956e70d2c471555c31.tar.gz vericert-7eeb169b982af90fac9873956e70d2c471555c31.zip | |
Finish some proofs and remove unnecessary Admitted
Diffstat (limited to 'src/hls/GiblePargenproofEvaluable.v')
| -rw-r--r-- | src/hls/GiblePargenproofEvaluable.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/hls/GiblePargenproofEvaluable.v b/src/hls/GiblePargenproofEvaluable.v index 84e7200..3bb9c66 100644 --- a/src/hls/GiblePargenproofEvaluable.v +++ b/src/hls/GiblePargenproofEvaluable.v @@ -284,7 +284,7 @@ Proof. unfold predicated_prod in *. exploit all_evaluable_map_and. 2: { eauto. } intros. 2: { eauto. } -Admitted. (* Requires simple lemma to prove, but this lemma is not needed. *) +Abort. (* Requires simple lemma to prove, but this lemma is not needed. *) Lemma cons_pred_expr_evaluable : forall G (ctx: @ctx G) ps a b, @@ -294,8 +294,8 @@ Lemma cons_pred_expr_evaluable : Proof. unfold cons_pred_expr; intros. apply all_evaluable_predicated_map. - now apply all_evaluable_predicated_prod. -Qed. + (*now apply all_evaluable_predicated_prod.*) +Abort. Lemma fold_right_all_evaluable : forall G (ctx: @ctx G) ps n, @@ -303,10 +303,10 @@ Lemma fold_right_all_evaluable : all_evaluable ctx ps (NE.fold_right cons_pred_expr (NE.singleton (T, Enil)) n). Proof. induction n; cbn in *; intros. - - unfold cons_pred_expr. eapply all_evaluable_predicated_map. eapply all_evaluable_predicated_prod. - inv H. auto. unfold all_evaluable; intros. inv H0. exists true. constructor. - - inv H. specialize (IHn H3). now eapply cons_pred_expr_evaluable. -Qed. + - unfold cons_pred_expr. eapply all_evaluable_predicated_map. (*eapply all_evaluable_predicated_prod. + inv H. auto. unfold all_evaluable; intros. inv H0. exists true. constructor.*) admit. + - inv H. specialize (IHn H3). (*now eapply cons_pred_expr_evaluable.*) +Abort. Lemma merge_all_evaluable : forall G (ctx: @ctx G) ps, |