diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-09 10:10:05 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-09 10:10:05 +0100 |
| commit | c1778dc2f1a5de755b32f8c4655a718c109c6489 (patch) | |
| tree | 826185424f8e081203b392824781f84a7bb58cfe /src/hls/GiblePargen.v | |
| parent | bad5c59b014a9baf18df0e2146edcb11fb931216 (diff) | |
| download | vericert-c1778dc2f1a5de755b32f8c4655a718c109c6489.tar.gz vericert-c1778dc2f1a5de755b32f8c4655a718c109c6489.zip | |
Split proof up into more files
Diffstat (limited to 'src/hls/GiblePargen.v')
| -rw-r--r-- | src/hls/GiblePargen.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 3000211..2c7bfc8 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -36,6 +36,8 @@ Require Import vericert.hls.Gible. Require Import vericert.hls.Predicate. Require Import vericert.hls.Abstr. Require Import vericert.common.DecEq. +Require Import vericert.hls.GiblePargenproofEquiv. + Import NE.NonEmptyNotation. #[local] Open Scope positive. @@ -80,6 +82,31 @@ Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) := Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A) : predicated B := NE.map (fun x => (fst x, f (snd x))) p. +Lemma NEin_map : + forall A B p y (f: A -> B) a, + NE.In (p, y) (predicated_map f a) -> + exists x, NE.In (p, x) a /\ y = f x. +Proof. + induction a; intros. + - inv H. destruct a. econstructor. split; eauto. constructor. + - inv H. inv H1. inv H. destruct a. cbn in *. econstructor; econstructor; eauto. + constructor; tauto. + specialize (IHa H). inv IHa. inv H0. + econstructor; econstructor; eauto. constructor; tauto. +Qed. + +Lemma NEin_map2 : + forall A B (f: A -> B) a p y, + NE.In (p, y) a -> + NE.In (p, f y) (predicated_map f a). +Proof. + induction a; crush. + inv H. constructor. + inv H. inv H1. + - constructor; auto. + - constructor; eauto. +Qed. + Definition cons_pred_expr (pel: pred_expr) (tpel: predicated expression_list) := predicated_map (uncurry Econs) (predicated_prod pel tpel). |