Skip to content

C
cpdt
Commit e1ab379e authored by Adam Chlipala's avatar Adam Chlipala
Browse files
Options

Parts I want to keep compile with 8.2

parent 7e33bd55
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 41 additions and 1519 deletions
.hgignore
View file @ e1ab379e
......@@ -18,3 +18,6 @@ templates/*.v
staging/html/.dir
cpdt.tgz
*.glob
*.v.d
Makefile
View file @ e1ab379e
MODULES_NODOC := Axioms AxiomsImpred Tactics MoreSpecif DepList
MODULES_NODOC := Axioms Tactics MoreSpecif DepList
MODULES_PROSE := Intro
MODULES_CODE := StackMachine InductiveTypes Predicates Coinductive Subset \
MoreDep DataStruct Equality Match Reflection Firstorder Hoas Interps \
......@@ -17,7 +17,7 @@ coq: Makefile.coq
Makefile.coq: Makefile $(VS)
coq_makefile $(VS) \
COQC = "coqc -impredicative-set -I src -dump-glob $(GLOBALS)" \
COQC = "coqc -I src -dump-glob $(GLOBALS)" \
COQDEP = "coqdep -I src" \
-o Makefile.coq
......
src/DataStruct.v
View file @ e1ab379e
......@@ -699,7 +699,7 @@ Section cfoldCond.
match n return (findex n -> exp' Bool) -> (findex n -> exp' t) -> exp' t with
| O => fun _ _ => default
| S n' => fun tests bodies =>
match tests None with
match tests None return _ with
| BConst true => bodies None
| BConst false => cfoldCond n'
(fun idx => tests (Some idx))
......@@ -743,14 +743,14 @@ Fixpoint cfold t (e : exp' t) {struct e} : exp' t :=
| Plus e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' with
match e1', e2' return _ with
| NConst n1, NConst n2 => NConst (n1 + n2)
| _, _ => Plus e1' e2'
end
| Eq e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' with
match e1', e2' return _ with
| NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
| _, _ => Eq e1' e2'
end
......
src/Extensional.v
View file @ e1ab379e
......@@ -963,6 +963,7 @@ Module PatMatch.
| [ H : forall env, Some _ = Some env -> _ |- _ ] =>
destruct (H _ (refl_equal _)); clear H; intuition
| [ H : _ |- _ ] => rewrite H; intuition
| [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] => destruct v; auto
end.
Qed.
......
src/Impure.v
View file @ e1ab379e
......@@ -7,232 +7,8 @@
* http://creativecommons.org/licenses/by-nc-nd/3.0/
*)
(* begin hide *)
Require Import Arith List Omega.
Require Import Axioms Tactics.
Set Implicit Arguments.
(* end hide *)
(** %\chapter{Modeling Impure Languages}% *)
(** TODO: Prose for this chapter *)
Section var.
Variable var : Type.
Inductive term : Type :=
| Var : var -> term
| App : term -> term -> term
| Abs : (var -> term) -> term
| Unit : term.
End var.
Implicit Arguments Unit [var].
Notation "# v" := (Var v) (at level 70).
Notation "()" := Unit.
Infix "@" := App (left associativity, at level 72).
Notation "\ x , e" := (Abs (fun x => e)) (at level 73).
Notation "\ ? , e" := (Abs (fun _ => e)) (at level 73).
Definition Term := forall var, term var.
Definition ident : Term := fun _ => \x, #x.
Definition unite : Term := fun _ => ().
Definition ident_self : Term := fun _ => ident _ @ ident _.
Definition ident_unit : Term := fun _ => ident _ @ unite _.
Module impredicative.
Inductive dynamic : Set :=
| Dyn : forall (dynTy : Type), dynTy -> dynamic.
Inductive computation (T : Type) : Set :=
| Return : T -> computation T
| Bind : forall (T' : Type),
computation T' -> (T' -> computation T) -> computation T
| Unpack : dynamic -> computation T.
Inductive eval : forall T, computation T -> T -> Prop :=
| EvalReturn : forall T (v : T),
eval (Return v) v
| EvalUnpack : forall T (v : T),
eval (Unpack T (Dyn v)) v
| EvalBind : forall T1 T2 (c1 : computation T1) (c2 : T1 -> computation T2) v1 v2,
eval c1 v1
-> eval (c2 v1) v2
-> eval (Bind c1 c2) v2.
(* begin thide *)
Fixpoint termDenote (e : term dynamic) : computation dynamic :=
match e with
| Var v => Return v
| App e1 e2 => Bind (termDenote e1) (fun f =>
Bind (termDenote e2) (fun x =>
Bind (Unpack (dynamic -> computation dynamic) f) (fun f' =>
f' x)))
| Abs e' => Return (Dyn (fun x => termDenote (e' x)))
| Unit => Return (Dyn tt)
end.
(* end thide *)
Definition TermDenote (E : Term) := termDenote (E _).
Eval compute in TermDenote ident.
Eval compute in TermDenote unite.
Eval compute in TermDenote ident_self.
Eval compute in TermDenote ident_unit.
Theorem eval_ident_unit : eval (TermDenote ident_unit) (Dyn tt).
(* begin thide *)
compute.
repeat econstructor.
simpl.
constructor.
Qed.
(* end thide *)
Theorem invert_ident : forall (E : Term) d,
eval (TermDenote (fun _ => ident _ @ E _)) d
-> eval (TermDenote E) d.
(* begin thide *)
inversion 1.
crush.
Focus 3.
crush.
unfold TermDenote in H0.
simpl in H0.
(** [injection H0.] *)
Abort.
(* end thide *)
End impredicative.
Module predicative.
Inductive val : Type :=
| Func : nat -> val
| VUnit.
Inductive computation : Type :=
| Return : val -> computation
| Bind : computation -> (val -> computation) -> computation
| CAbs : (val -> computation) -> computation
| CApp : val -> val -> computation.
Definition func := val -> computation.
Fixpoint get (n : nat) (ls : list func) {struct ls} : option func :=
match ls with
| nil => None
| x :: ls' =>
if eq_nat_dec n (length ls')
then Some x
else get n ls'
end.
Inductive eval : list func -> computation -> list func -> val -> Prop :=
| EvalReturn : forall ds d,
eval ds (Return d) ds d
| EvalBind : forall ds c1 c2 ds' d1 ds'' d2,
eval ds c1 ds' d1
-> eval ds' (c2 d1) ds'' d2
-> eval ds (Bind c1 c2) ds'' d2
| EvalCAbs : forall ds f,
eval ds (CAbs f) (f :: ds) (Func (length ds))
| EvalCApp : forall ds i d2 f ds' d3,
get i ds = Some f
-> eval ds (f d2) ds' d3
-> eval ds (CApp (Func i) d2) ds' d3.
(* begin thide *)
Fixpoint termDenote (e : term val) : computation :=
match e with
| Var v => Return v
| App e1 e2 => Bind (termDenote e1) (fun f =>
Bind (termDenote e2) (fun x =>
CApp f x))
| Abs e' => CAbs (fun x => termDenote (e' x))
| Unit => Return VUnit
end.
(* end thide *)
Definition TermDenote (E : Term) := termDenote (E _).
Eval compute in TermDenote ident.
Eval compute in TermDenote unite.
Eval compute in TermDenote ident_self.
Eval compute in TermDenote ident_unit.
Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit.
(* begin thide *)
compute.
repeat econstructor.
simpl.
rewrite (eta Return).
reflexivity.
Qed.
Hint Constructors eval.
Lemma app_nil_start : forall A (ls : list A),
ls = nil ++ ls.
reflexivity.
Qed.
Lemma app_cons : forall A (x : A) (ls : list A),
x :: ls = (x :: nil) ++ ls.
reflexivity.
Qed.
Theorem eval_monotone : forall ds c ds' d,
eval ds c ds' d
-> exists ds'', ds' = ds'' ++ ds.
Hint Resolve app_nil_start app_ass app_cons.
induction 1; firstorder; subst; eauto.
Qed.
Lemma length_app : forall A (ds2 ds1 : list A),
length (ds1 ++ ds2) = length ds1 + length ds2.
induction ds1; simpl; intuition.
Qed.
Lemma get_app : forall ds2 d ds1,
get (length ds2) (ds1 ++ d :: ds2) = Some d.
Hint Rewrite length_app : cpdt.
induction ds1; crush;
match goal with
| [ |- context[if ?E then _ else _] ] => destruct E
end; crush.
Qed.
(* end thide *)
Theorem invert_ident : forall (E : Term) ds ds' d,
eval ds (TermDenote (fun _ => ident _ @ E _)) ds' d
-> eval ((fun x => Return x) :: ds) (TermDenote E) ds' d.
(* begin thide *)
inversion 1; subst.
clear H.
inversion H3; clear H3; subst.
inversion H6; clear H6; subst.
generalize (eval_monotone H2); crush.
inversion H5; clear H5; subst.
rewrite get_app in H3.
inversion H3; clear H3; subst.
inversion H7; clear H7; subst.
assumption.
Qed.
(* end thide *)
End predicative.
(** TODO: This chapter! (Old version was too impredicative) *)
src/Intensional.v
View file @ e1ab379e
This diff is collapsed.
src/Interps.v
View file @ e1ab379e
......@@ -10,7 +10,7 @@
(* begin hide *)
Require Import String List.
Require Import AxiomsImpred Tactics.
Require Import Axioms Tactics.
Set Implicit Arguments.
(* end hide *)
......@@ -121,7 +121,7 @@ Module STLC.
| Plus e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' with
match e1', e2' return _ with
| Const n1, Const n2 => ^(n1 + n2)
| _, _ => e1' +^ e2'
end
......@@ -301,7 +301,7 @@ Module PSLC.
Variable var : type -> Type.
Definition pairOutType t :=
match t with
match t return Type with
| t1 ** t2 => option (exp var t1 * exp var t2)
| _ => unit
end.
......@@ -326,7 +326,7 @@ Module PSLC.
| Plus e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' with
match e1', e2' return _ with
| Const n1, Const n2 => ^(n1 + n2)
| _, _ => e1' +^ e2'
end
......@@ -392,196 +392,3 @@ Module PSLC.
Qed.
(* end thide *)
End PSLC.
(** * Type Variables *)
Module SysF.
(* EX: Follow a similar progression for System F. *)
(* begin thide *)
Section vars.
Variable tvar : Type.
Inductive type : Type :=
| Nat : type
| Arrow : type -> type -> type
| TVar : tvar -> type
| All : (tvar -> type) -> type.
Notation "## v" := (TVar v) (at level 40).
Infix "-->" := Arrow (right associativity, at level 60).
Section Subst.
Variable t : type.
Inductive Subst : (tvar -> type) -> type -> Prop :=
| SNat : Subst (fun _ => Nat) Nat
| SArrow : forall dom ran dom' ran',
Subst dom dom'
-> Subst ran ran'
-> Subst (fun v => dom v --> ran v) (dom' --> ran')
| SVarEq : Subst TVar t
| SVarNe : forall v, Subst (fun _ => ##v) (##v)
| SAll : forall ran ran',
(forall v', Subst (fun v => ran v v') (ran' v'))
-> Subst (fun v => All (ran v)) (All ran').
End Subst.
Variable var : type -> Type.
Inductive exp : type -> Type :=
| Var : forall t,
var t
-> exp t
| Const : nat -> exp Nat
| Plus : exp Nat -> exp Nat -> exp Nat
| App : forall t1 t2,
exp (t1 --> t2)
-> exp t1
-> exp t2
| Abs : forall t1 t2,
(var t1 -> exp t2)
-> exp (t1 --> t2)
| TApp : forall tf,
exp (All tf)
-> forall t tf', Subst t tf tf'
-> exp tf'
| TAbs : forall tf,
(forall v, exp (tf v))
-> exp (All tf).
End vars.
Definition Typ := forall tvar, type tvar.
Definition Exp (T : Typ) := forall tvar (var : type tvar -> Type), exp var (T _).
(* end thide *)
Implicit Arguments Nat [tvar].
Notation "## v" := (TVar v) (at level 40).
Infix "-->" := Arrow (right associativity, at level 60).
Notation "\\\ x , t" := (All (fun x => t)) (at level 65).
Implicit Arguments Var [tvar var t].
Implicit Arguments Const [tvar var].
Implicit Arguments Plus [tvar var].
Implicit Arguments App [tvar var t1 t2].
Implicit Arguments Abs [tvar var t1 t2].
Implicit Arguments TAbs [tvar var tf].
Notation "# v" := (Var v) (at level 70).
Notation "^ n" := (Const n) (at level 70).
Infix "+^" := Plus (left associativity, at level 79).
Infix "@" := App (left associativity, at level 77).
Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
Notation "e @@ t" := (TApp e (t := t) _) (left associativity, at level 77).
Notation "\\ x , e" := (TAbs (fun x => e)) (at level 78).
Notation "\\ ! , e" := (TAbs (fun _ => e)) (at level 78).
Definition zero : Exp (fun _ => Nat) := fun _ _ =>
^0.
Definition ident : Exp (fun _ => \\\T, ##T --> ##T) := fun _ _ =>
\\T, \x, #x.
Definition ident_zero : Exp (fun _ => Nat).
do 2 intro; refine (ident _ @@ _ @ zero _);
repeat constructor.
Defined.
Definition ident_ident : Exp (fun _ => \\\T, ##T --> ##T).
do 2 intro; refine (ident _ @@ _ @ ident _);
repeat constructor.
Defined.
Definition ident5 : Exp (fun _ => \\\T, ##T --> ##T).
do 2 intro; refine (ident_ident _ @@ _ @ ident_ident _ @@ _ @ ident _);
repeat constructor.
Defined.
(* begin thide *)
Fixpoint typeDenote (t : type Set) : Set :=
match t with
| Nat => nat
| t1 --> t2 => typeDenote t1 -> typeDenote t2
| ##v => v
| All tf => forall T, typeDenote (tf T)
end.
Lemma Subst_typeDenote : forall t tf tf',
Subst t tf tf'
-> typeDenote (tf (typeDenote t)) = typeDenote tf'.
induction 1; crush; ext_eq; crush.
Defined.
Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
match e in (exp _ t) return (typeDenote t) with
| Var _ v => v
| Const n => n
| Plus e1 e2 => expDenote e1 + expDenote e2
| App _ _ e1 e2 => (expDenote e1) (expDenote e2)
| Abs _ _ e' => fun x => expDenote (e' x)
| TApp _ e' t' _ pf => match Subst_typeDenote pf in _ = T return T with
| refl_equal => (expDenote e') (typeDenote t')
end
| TAbs _ e' => fun T => expDenote (e' T)
end.
Definition ExpDenote T (E : Exp T) := expDenote (E _ _).
(* end thide *)
Eval compute in ExpDenote zero.
Eval compute in ExpDenote ident.
Eval compute in ExpDenote ident_zero.
Eval compute in ExpDenote ident_ident.
Eval compute in ExpDenote ident5.
(* begin thide *)
Section cfold.
Variable tvar : Type.
Variable var : type tvar -> Type.
Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
match e in exp _ t return exp _ t with
| Var _ v => #v
| Const n => ^n
| Plus e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' with
| Const n1, Const n2 => ^(n1 + n2)
| _, _ => e1' +^ e2'
end
| App _ _ e1 e2 => cfold e1 @ cfold e2
| Abs _ _ e' => Abs (fun x => cfold (e' x))
| TApp _ e' _ _ pf => TApp (cfold e') pf
| TAbs _ e' => \\T, cfold (e' T)
end.
End cfold.
Definition Cfold T (E : Exp T) : Exp T := fun _ _ => cfold (E _ _).
Lemma cfold_correct : forall t (e : exp _ t),
expDenote (cfold e) = expDenote e.
induction e; crush; try (ext_eq; crush);
repeat (match goal with
| [ |- context[cfold ?E] ] => dep_destruct (cfold E)
end; crush).
Qed.
Theorem Cfold_correct : forall t (E : Exp t),
ExpDenote (Cfold E) = ExpDenote E.
unfold ExpDenote, Cfold; intros; apply cfold_correct.
Qed.
(* end thide *)
End SysF.
src/Match.v
View file @ e1ab379e
......@@ -784,10 +784,10 @@ Qed.
Ltac matcher :=
intros;
repeat search_prem ltac:(apply False_prem || (apply ex_prem; intro));
repeat search_conc ltac:(apply True_conc || eapply ex_conc
|| search_prem ltac:(apply Match));
try apply imp_True.
repeat search_prem ltac:(simple apply False_prem || (simple apply ex_prem; intro));
repeat search_conc ltac:(simple apply True_conc || simple eapply ex_conc
|| search_prem ltac:(simple apply Match));
try simple apply imp_True.
(* end thide *)
(** Our tactic succeeds at proving a simple example. *)
......
src/MoreDep.v
View file @ e1ab379e
......@@ -247,20 +247,20 @@ Definition pairOut t (e : exp t) :=
With [pairOut] available, we can write [cfold] in a straightforward way. There are really no surprises beyond that Coq verifies that this code has such an expressive type, given the small annotation burden. *)
Fixpoint cfold t (e : exp t) {struct e} : exp t :=
match e in (exp t) return (exp t) with
Fixpoint cfold t (e : exp t) : exp t :=
match e with
| NConst n => NConst n
| Plus e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' with
match e1', e2' return _ with
| NConst n1, NConst n2 => NConst (n1 + n2)
| _, _ => Plus e1' e2'
end
| Eq e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' with
match e1', e2' return _ with
| NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
| _, _ => Eq e1' e2'
end
......@@ -269,7 +269,7 @@ Fixpoint cfold t (e : exp t) {struct e} : exp t :=
| And e1 e2 =>
let e1' := cfold e1 in
let e2' := cfold e2 in
match e1', e2' with
match e1', e2' return _ with
| BConst b1, BConst b2 => BConst (b1 && b2)
| _, _ => And e1' e2'
end
......@@ -1028,7 +1028,7 @@ Section dec_star.
(** Finally, we have [dec_star]. It has a straightforward implementation. We introduce a spurious match on [s] so that [simpl] will know to reduce calls to [dec_star]. The heuristic that [simpl] uses is only to unfold identifier definitions when doing so would simplify some [match] expression. *)
Definition dec_star : {star P s} + { ~star P s}.
refine (match s with
refine (match s return _ with
| "" => Reduce (dec_star' (n := length s) 0 _)
| _ => Reduce (dec_star' (n := length s) 0 _)
end); crush.
......
src/Subset.v
View file @ e1ab379e
......@@ -376,7 +376,7 @@ let rec eq_nat_dec' n m0 =
We can build "smart" versions of the usual boolean operators and put them to good use in certified programming. For instance, here is a [sumbool] version of boolean "or." *)
(* begin thide *)
Notation "x || y" := (if x then Yes else Reduce y) (at level 50).
Notation "x || y" := (if x then Yes else Reduce y).
(** Let us use it for building a function that decides list membership. We need to assume the existence of an equality decision procedure for the type of list elements. *)
......
src/Tactics.v
View file @ e1ab379e
......@@ -48,15 +48,21 @@ Ltac simplHyp invOne :=
match goal with
| [ H : ex _ |- _ ] => destruct H
| [ H : ?F ?X = ?F ?Y |- _ ] => injection H;
match goal with
| [ |- F X = F Y -> _ ] => fail 1
| [ |- _ = _ -> _ ] => try clear H; intros; try subst
end
| [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
match goal with
| [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst
end
| [ H : ?F ?X = ?F ?Y |- ?G ] =>
(assert (X = Y); [ assumption | fail 1 ])
|| (injection H;
match goal with
| [ |- X = Y -> G ] =>
try clear H; intros; try subst
end)
| [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
(assert (X = Y); [ assumption
| assert (U = V); [ assumption | fail 1 ] ])
|| (injection H;
match goal with
| [ |- U = V -> X = Y -> G ] =>
try clear H; intros; try subst
end)
| [ H : ?F _ |- _ ] => invert H F
| [ H : ?F _ _ |- _ ] => invert H F
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment