Mercurial > urweb

comparison src/coq/Semantics.v @ 1618:705cb41ac7d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update Coq semantics for 8.3pl2
author Adam Chlipala <adam@chlipala.net>
date Wed, 30 Nov 2011 15:28:56 -0500
parents 75c7a69354d6
children
comparison
equal deleted inserted replaced
1617:8611da277df4 1618:705cb41ac7d0
1 (* Copyright (c) 2009, Adam Chlipala 1 (* Copyright (c) 2009, 2011, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE. 25 * POSSIBILITY OF SUCH DAMAGE.
26 *) 26 *)
27 27
28 Require Import Eqdep. 28 Require Import Eqdep_dec.
29 29
30 Require Import Axioms. 30 Require Import Axioms.
31 Require Import Syntax. 31 Require Import Syntax.
32 32
33 Set Implicit Arguments. 33 Set Implicit Arguments.
52 forall n, match r1 n, r2 n with 52 forall n, match r1 n, r2 n with
53 | Some _, Some _ => False 53 | Some _, Some _ => False
54 | _, _ => True 54 | _, _ => True
55 end. 55 end.
56 56
57 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k := 57 Fixpoint cDen k (c : con kDen k) : kDen k :=
58 match c in con _ k return kDen k with 58 match c with
59 | CVar _ x => x 59 | CVar _ x => x
60 | Arrow c1 c2 => cDen c1 -> cDen c2 60 | Arrow c1 c2 => cDen c1 -> cDen c2
61 | Poly _ c1 => forall x, cDen (c1 x) 61 | Poly _ c1 => forall x, cDen (c1 x)
62 | CAbs _ _ c1 => fun x => cDen (c1 x) 62 | CAbs _ _ c1 => fun x => cDen (c1 x)
63 | CApp _ _ c1 c2 => (cDen c1) (cDen c2) 63 | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
145 Definition tDen (t : con kDen KType) : Set := cDen t. 145 Definition tDen (t : con kDen KType) : Set := cDen t.
146 146
147 Theorem name_eq_dec_refl : forall n, name_eq_dec n n = left _ (refl_equal n). 147 Theorem name_eq_dec_refl : forall n, name_eq_dec n n = left _ (refl_equal n).
148 intros; destruct (name_eq_dec n n); intuition; [ 148 intros; destruct (name_eq_dec n n); intuition; [
149 match goal with 149 match goal with
150 | [ e : _ = _ |- _ ] => rewrite (UIP_refl _ _ e); reflexivity 150 | [ e : _ = _ |- _ ] => rewrite (UIP_dec name_eq_dec e (refl_equal _)); reflexivity
151 end 151 end
152 | elimtype False; tauto 152 | elimtype False; tauto
153 ]. 153 ].
154 Qed. 154 Qed.
155 155
166 destruct (r n1); intuition. 166 destruct (r n1); intuition.
167 Qed. 167 Qed.
168 168
169 Implicit Arguments cut_disjoint [v r]. 169 Implicit Arguments cut_disjoint [v r].
170 170
171 Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t := 171 Fixpoint eDen t (e : exp dvar tDen t) : tDen t :=
172 match e in exp _ _ t return tDen t with 172 match e in exp _ _ t return tDen t with
173 | Var _ x => x 173 | Var _ x => x
174 | App _ _ e1 e2 => (eDen e1) (eDen e2) 174 | App _ _ e1 e2 => (eDen e1) (eDen e2)
175 | Abs _ _ e1 => fun x => eDen (e1 x) 175 | Abs _ _ e1 => fun x => eDen (e1 x)
176 | ECApp _ c _ _ e1 Hsub => match subs_correct Hsub in _ = T return T with 176 | ECApp _ c _ _ e1 Hsub => match subs_correct Hsub in _ = T return T with
179 | ECAbs _ _ e1 => fun X => eDen (e1 X) 179 | ECAbs _ _ e1 => fun X => eDen (e1 X)
180 | Cast _ _ Heq e1 => match deq_correct Heq in _ = T return T with 180 | Cast _ _ Heq e1 => match deq_correct Heq in _ = T return T with
181 | refl_equal => eDen e1 181 | refl_equal => eDen e1
182 end 182 end
183 | Empty => fun _ => tt 183 | Empty => fun _ => tt
184 | Single c _ e1 => fun n => if name_eq_dec n (cDen c) as B 184 | Single c c' e1 => fun n => if name_eq_dec n (cDen c) as B
185 return (match (match (if B then _ else _) with Some _ => if B then _ else _ | None => _ end) 185 return (match (match (if B then _ else _) with Some _ => _ | None => _ end)
186 with Some _ => _ | None => unit end) 186 with Some _ => _ | None => unit end)
187 then eDen e1 else tt 187 then eDen e1 else tt
188 | Proj c _ _ e1 => 188 | Proj c _ _ e1 =>
189 match name_eq_dec_refl (cDen c) in _ = B 189 match name_eq_dec_refl (cDen c) in _ = B
190 return (match (match (if B then _ else _) with 190 return (match (match (if B then _ else _) with
191 | Some _ => if B then _ else _ 191 | Some _ => _
192 | None => _ end) 192 | None => _ end)
193 return Set 193 return Set
194 with Some _ => _ | None => _ end) with 194 with Some _ => _ | None => _ end) with
195 | refl_equal => (eDen e1) (cDen c) 195 | refl_equal => (eDen e1) (cDen c)
196 end 196 end
197 | Cut c _ c' Hdisj e1 => fun n => 197 | Cut c _ c' Hdisj e1 => fun n =>
198 match name_eq_dec n (cDen c) as B return (match (match (if B then Some _ else None) with Some _ => if B then _ else _ | None => (cDen c') n end) 198 match name_eq_dec n (cDen c) as B return (match (match (if B then Some _ else None) with Some _ => _ | None => (cDen c') n end)
199 with Some T => T | None => unit end 199 with Some T => T | None => unit end
200 -> match (cDen c') n with 200 -> match (cDen c') n with
201 | None => unit 201 | None => unit
202 | Some T => T 202 | Some T => T
203 end) with 203 end) with
216 | None => unit 216 | None => unit
217 | Some T => T 217 | Some T => T
218 end 218 end
219 -> match (match D with 219 -> match (match D with
220 | None => (cDen c2) n 220 | None => (cDen c2) n
221 | v => v 221 | Some v => Some v
222 end) with 222 end) with
223 | None => unit 223 | None => unit
224 | Some T => T 224 | Some T => T
225 end with 225 end with
226 | None => fun _ => (eDen e2) n 226 | None => fun _ => (eDen e2) n