From 42d5af6d2dc208a2c39db9c76c9d380472b3de49 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 26 Apr 2020 14:29:53 -0400 Subject: [PATCH] Revising before class --- ProgramDerivation_template.v | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/ProgramDerivation_template.v b/ProgramDerivation_template.v index 566ea1b..f7e368f 100644 --- a/ProgramDerivation_template.v +++ b/ProgramDerivation_template.v @@ -2,6 +2,8 @@ Require Import Frap. Require Import Program Setoids.Setoid Classes.RelationClasses Classes.Morphisms Morphisms_Prop. Require Import Eqdep. +Set Warnings "-cannot-define-projection". + Ltac inv_pair := match goal with | [ H : existT _ _ _ = existT _ _ _ |- _ ] => apply inj_pair2 in H; invert H @@ -185,7 +187,7 @@ Inductive RefineMethods {state1 state2} (R : state1 -> state2 -> Prop) -> RefineMethods R (MethodsCons {| MethodName := name; MethodBody := f1 |} ms1) (MethodsCons {| MethodName := name; MethodBody := f2 |} ms2). -Hint Constructors RefineMethods. +Hint Constructors RefineMethods : core. Record adt_refine {names} (adt1 adt2 : adt names) : Prop := { ArRel : AdtState adt1 -> AdtState adt2 -> Prop; @@ -212,7 +214,7 @@ Definition split_counter := ADT { and method "value"[[self, _]] = ret (self, fst self + snd self) }. -Hint Extern 1 (@eq nat _ _) => simplify; linear_arithmetic. +Hint Extern 1 (@eq nat _ _) => simplify; linear_arithmetic : core. Theorem split_counter_ok : adt_refine counter split_counter. Proof. @@ -230,7 +232,7 @@ Proof. subst; eauto. Qed. -Hint Immediate RefineMethods_refl. +Hint Immediate RefineMethods_refl : core. Theorem refine_refl : forall names (adt1 : adt names), adt_refine adt1 adt1. @@ -259,7 +261,7 @@ Proof. first_order. Qed. -Hint Resolve RefineMethods_trans. +Hint Resolve RefineMethods_trans : core. Theorem refine_trans : forall names (adt1 adt2 adt3 : adt names), adt_refine adt1 adt2 @@ -322,7 +324,7 @@ Proof. simplify; subst; eauto. Qed. -Hint Resolve ReplaceMethod_ok. +Hint Resolve ReplaceMethod_ok : core. Theorem refine_method : forall state name (oldbody newbody : state -> nat -> comp (state * nat)) names (ms1 ms2 : methods state names) constr, @@ -367,7 +369,7 @@ Proof. eauto. Qed. -Hint Resolve RepChangeMethods_ok. +Hint Resolve RepChangeMethods_ok : core. Theorem refine_rep : forall state1 state2 (absfunc : state2 -> state1) names (ms1 : methods state1 names) (ms2 : methods state2 names) @@ -424,7 +426,7 @@ Inductive CachingMethods {state} (name : string) (func : state -> nat) CachingMethods name func ms1 ms2 -> CachingMethods name func (MethodsCons {| MethodName := name; MethodBody := (fun s _ => ret (s, func s)) |} ms1) - (MethodsCons {| MethodName := name; MethodBody := (fun s arg => ret (s, snd s)) |} ms2) + (MethodsCons {| MethodName := name; MethodBody := (fun s _ => ret (s, snd s)) |} ms2) | CmDefault : forall name' names oldbody (ms1 : methods state names) (ms2 : methods _ names), name' <> name -> CachingMethods name func ms1 ms2 @@ -458,7 +460,7 @@ Proof. eauto. Qed. -Hint Resolve CachingMethods_ok. +Hint Resolve CachingMethods_ok : core. Theorem refine_cache : forall state name (func : state -> nat) names (ms1 : methods state names) (ms2 : methods (state * nat) names)