From 0a15dc1ebeacd8a4dcac4a17493f9acbbc8d672e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 20 Jan 2024 16:31:37 +0000 Subject: [PATCH] Remove some commented Admitted lemmas --- src/Compiler.v | 12 ------------ src/hls/DHTLgenproof.v | 43 ------------------------------------------ 2 files changed, 55 deletions(-) diff --git a/src/Compiler.v b/src/Compiler.v index 53cde6a..45a7657 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -184,18 +184,6 @@ Proof. - red; intros. subst tp1 tp2. exists p; auto. Qed. -(* Global Instance TransfIfLink {A: Type} {LA: Linker A} *) -(* (transf: A -> A -> Prop) (TL: TransfLink transf) *) -(* : TransfLink (match_rep transf). *) -(* Admitted. *) - -(* Lemma total_rep_match: *) -(* forall (A B: Type) (n: list B) (f: A -> B -> A) *) -(* (rel: A -> A -> Prop) (prog: A), *) -(* (forall b p, rel p (f p b)) -> *) -(* match_rep rel prog (fold_left f n prog). *) -(* Proof. Admitted. *) - Lemma total_if_match: forall (A: Type) (flag: unit -> bool) (f: A -> A) (rel: A -> A -> Prop) (prog: A), diff --git a/src/hls/DHTLgenproof.v b/src/hls/DHTLgenproof.v index 3fda0c2..21f26e7 100644 --- a/src/hls/DHTLgenproof.v +++ b/src/hls/DHTLgenproof.v @@ -2364,49 +2364,6 @@ Proof. eapply PTree.elements_correct; eauto. Qed. - (* Lemma lt_max_resources_in_block : *) - (* forall bb a pc x x0, *) - (* In x (concat bb) -> *) - (* In x0 (pred_uses x) -> *) - (* Ple x0 (max_pred_block a pc bb). *) - (* Proof. *) - (* induction bb. *) - (* - intros. cbn in *. inv H. *) - (* - intros. cbn in *. *) - - (* Lemma lt_max_resources_lt_a : *) - (* forall bb x x0 a k v, *) - (* In x (concat bb) -> *) - (* In x0 (pred_uses x) -> *) - (* Ple x0 a -> *) - (* Ple x0 (max_pred_block a k v). *) - (* Proof. Admitted. *) - - (* Definition inductive_p final fld := *) - (* forall pc bb, *) - (* final ! pc = Some bb -> *) - (* Forall (fun i0 : instr => Forall (fun x2 : positive => Ple x2 fld) (pred_uses i0)) (concat bb). *) - - (* Lemma lt_max_resource_predicate_Forall : *) - (* forall f pc bb, *) - (* f.(GibleSubPar.fn_code) ! pc = Some bb -> *) - (* Forall (fun i0 : instr => Forall (fun x2 : positive => Ple x2 (max_pred_function f)) (pred_uses i0)) (concat bb). *) - (* Proof. *) - (* unfold max_pred_function. *) - (* intro f. *) - (* match goal with |- ?g => replace g with (inductive_p (fn_code f) (PTree.fold max_pred_block (fn_code f) 1%positive)) by auto end. *) - (* eapply PTree_Properties.fold_rec; unfold inductive_p; intros; cbn in *. *) - (* - eapply H0. erewrite H. eauto. *) - (* - now rewrite PTree.gempty in H. *) - (* - destruct (peq k pc); subst. *) - (* + rewrite PTree.gss in H2. inv H2. *) - (* eapply Forall_forall; intros. eapply Forall_forall; intros. eauto using lt_max_resources_in_block. *) - (* + rewrite PTree.gso in H2 by auto. *) - (* eapply H1 in H2. eapply Forall_forall; intros. eapply Forall_forall; intros. *) - (* eapply Forall_forall in H2; eauto. eapply Forall_forall in H2; eauto. *) - (* eauto using lt_max_resources_lt_a. *) - (* Qed. *) - Lemma lt_max_resource_predicate_Forall : forall f pc bb, f.(GibleSubPar.fn_code) ! pc = Some bb ->