Mercurial > cpdt > repo

comparison src/ProgLang.v @ 568:81d63d9c1cc5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port to Coq 8.9.0
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Jan 2019 15:16:29 -0500
parents dac7a2705b00
children 0ce9829efa3b
comparison
equal deleted inserted replaced
567:ec0ce5129fc4 568:81d63d9c1cc5
103 | Abs : forall G dom ran, term (dom :: G) ran -> term G (Func dom ran) 103 | Abs : forall G dom ran, term (dom :: G) ran -> term G (Func dom ran)
104 | App : forall G dom ran, term G (Func dom ran) -> term G dom -> term G ran 104 | App : forall G dom ran, term G (Func dom ran) -> term G dom -> term G ran
105 105
106 | Let : forall G t1 t2, term G t1 -> term (t1 :: G) t2 -> term G t2. 106 | Let : forall G t1 t2, term G t1 -> term (t1 :: G) t2 -> term G t2.
107 107
108 Implicit Arguments Const [G]. 108 Arguments Const [G].
109 109
110 (** Here are two example term encodings, the first of addition packaged as a two-argument curried function, and the second of a sample application of addition to constants. *) 110 (** Here are two example term encodings, the first of addition packaged as a two-argument curried function, and the second of a sample application of addition to constants. *)
111 111
112 Example add : term nil (Func Nat (Func Nat Nat)) := 112 Example add : term nil (Func Nat (Func Nat Nat)) :=
113 Abs (Abs (Plus (Var (HNext HFirst)) (Var HFirst))). 113 Abs (Abs (Plus (Var (HNext HFirst)) (Var HFirst))).
264 | nil => fun s => x ::: s 264 | nil => fun s => x ::: s
265 | t' :: G' => fun s => hhd s ::: insertAtS t x n' (htl s) 265 | t' :: G' => fun s => hhd s ::: insertAtS t x n' (htl s)
266 end 266 end
267 end. 267 end.
268 268
269 Implicit Arguments insertAtS [t G]. 269 Arguments insertAtS [t] x [G].
270 270
271 (** Next we prove that [liftVar] is correct. That is, a lifted variable retains its value with respect to a substitution when we perform an analogue to lifting by inserting a new mapping into the substitution. *) 271 (** Next we prove that [liftVar] is correct. That is, a lifted variable retains its value with respect to a substitution when we perform an analogue to lifting by inserting a new mapping into the substitution. *)
272 272
273 Lemma liftVarSound : forall t' (x : typeDenote t') t G (m : member t G) s n, 273 Lemma liftVarSound : forall t' (x : typeDenote t') t G (m : member t G) s n,
274 hget s m = hget (insertAtS x n s) (liftVar m t' n). 274 hget s m = hget (insertAtS x n s) (liftVar m t' n).
353 | App : forall dom ran, term (Func dom ran) -> term dom -> term ran 353 | App : forall dom ran, term (Func dom ran) -> term dom -> term ran
354 354
355 | Let : forall t1 t2, term t1 -> (var t1 -> term t2) -> term t2. 355 | Let : forall t1 t2, term t1 -> (var t1 -> term t2) -> term t2.
356 End var. 356 End var.
357 357
358 Implicit Arguments Var [var t]. 358 Arguments Var [var t].
359 Implicit Arguments Const [var]. 359 Arguments Const [var].
360 Implicit Arguments Abs [var dom ran]. 360 Arguments Abs [var dom ran].
361 361
362 (** Coq accepts this definition because our embedded functions now merely take _variables_ as arguments, instead of arbitrary terms. One might wonder whether there is an easy loophole to exploit here, instantiating the parameter [var] as [term] itself. However, to do that, we would need to choose a variable representation for this nested mention of [term], and so on through an infinite descent into [term] arguments. 362 (** Coq accepts this definition because our embedded functions now merely take _variables_ as arguments, instead of arbitrary terms. One might wonder whether there is an easy loophole to exploit here, instantiating the parameter [var] as [term] itself. However, to do that, we would need to choose a variable representation for this nested mention of [term], and so on through an infinite descent into [term] arguments.
363 363
364 We write the final type of a closed term using polymorphic quantification over all possible choices of [var] type family. *) 364 We write the final type of a closed term using polymorphic quantification over all possible choices of [var] type family. *)
365 365