From 45124f3686e1a1903deec4c045d292bb072363cd Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 4 Apr 2021 14:51:02 -0400 Subject: [PATCH] Revising for Wednesday's lecture --- SubsetTypes.v | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/SubsetTypes.v b/SubsetTypes.v index 28a02f5..a9044b7 100644 --- a/SubsetTypes.v +++ b/SubsetTypes.v @@ -216,10 +216,8 @@ Definition pred_strong4 : forall (n : nat), n > 0 -> {m : nat | n = S m}. * to [False_rec], and the second subgoal comes from the second underscore * passed to [exist]. In the first case, we see that, though we bound the * proof variable with an underscore, it is still available in our proof - * context. It is hard to refer to underscore-named variables in manual - * proofs, but automation makes short work of them. Both subgoals are easy to - * discharge that way, so let us back up and ask to prove all subgoals - * automatically. *) + * context. Both subgoals are easy to discharge, so let us back up and ask to + * prove all subgoals automatically. *) Undo. refine (fun n => @@ -272,6 +270,10 @@ Compute pred_strong5 two_gt0. Print sumbool. +(* We have been using this type family behind the scenes for various equality + * checks, for instance: *) +Check "x" ==v "y". + (* Here, the constructors of [sumbool] have types written in terms of a * registered notation for [sumbool], such that the result type of each * constructor desugars to [sumbool A B]. We can define some notations of our @@ -534,7 +536,7 @@ Notation "e1 ;; e2" := (if e1 then e2 else ??) * [hasType] proof obligation, and [eauto] makes short work of them when we add * [hasType]'s constructors as hints. *) -Hint Constructors hasType. +Local Hint Constructors hasType. Definition typeCheck : forall e : exp, {{t | hasType e t}}. refine (fix F (e : exp) : {{t | hasType e t}} := @@ -587,7 +589,7 @@ Qed. (* Now we can define the type-checker. Its type expresses that it only fails on * untypable expressions. *) -Hint Resolve hasType_det. +Local Hint Resolve hasType_det. (* The lemma [hasType_det] will also be useful for proving proof obligations * with contradictory contexts. *)