Commit ca5dad93 authored by Paul Wild's avatar Paul Wild

update levels of headings

parent cb0161db
......@@ -3,9 +3,7 @@ Require Import ModuRes.Constr ModuRes.UPred ModuRes.COFE.
Require Import Omega.
Require Import Common.Language Common.Lib Binary.LogRel Binary.WeakSub.
(** * Compatibility Lemmas
Having proven the Weakening and Substitution properties we can now
(** Having proven the Weakening and Substitution properties we can now
turn to the proof of the Fundamental property, which is that every
well-typed term is logically related to itself. On the road to that
proof we once more encounter the Compatibility lemmas, which are
......
......@@ -16,7 +16,9 @@ Proof.
intros e e' HS HI; unfold flip in HS; simpl in HS; subst; assumption.
Qed.
(** ** Constructions
(** * Chapter 2. A binary logical relation for contextual approximation
** Constructions
We now turn to building a LR for contextual approximation, which is going to be
binary. As in the unary case, we first need to consider what the space [T] of
......
......@@ -3,13 +3,14 @@ Require Import ModuRes.Constr ModuRes.UPred ModuRes.COFE.
Require Import Omega List.
Require Import Common.Language Common.Lib Binary.LogRel Binary.WeakSub Binary.Compatibility.
(**
In this file, we prove a very simple free theorem using our logical relation:
(** ** A parametricity result
In this file, we prove a very simple free theorem using our logical relation:
- If [e] is a well-typed term of type [ ##0 ##0], then it approximates
the (polymorphic) identity function [id = Λ (λ #0)].
- If [e] is a well-typed term of type [ ##0 ##0], then it approximates
the (polymorphic) identity function [id = Λ (λ #0)].
We will prove that for such [e], [logrel 0 (e @ v) v t] for any [v] of type [t].
We will prove that for such [e], [logrel 0 (e @ v) v t] for any [v] of type [t].
*)
Open Scope lang_scope.
......
Require Import DBLib.DeBruijn DBLib.Environments.
Require Import Common.Language Common.Lib Common.Tactics.
(**
As an example application of the logical relation we are going
to give a Coq solution to exercise 2 from homework sheet 4 of
Lars Birkedal's course on "Semantics of programming languages".
In it, we are given two implementations of an abstract queue
datatype and need to show that one approximates the other.
In this file, we first formalize the two implementations as
faithfully as possible in our object language, and use the
[check_type] tactic from [Tactics.v] to show that the so
defined expressions have the correct types.
(** An example with queues
As an example application of the logical relation we are going
to give a Coq solution to exercise 2 from homework sheet 4 of
Lars Birkedal's course on "Semantics of programming languages".
In it, we are given two implementations of an abstract queue
datatype and need to show that one approximates the other.
In this file, we first formalize the two implementations as
faithfully as possible in our object language, and use the
[check_type] tactic from [Tactics.v] to show that the so
defined expressions have the correct types.
*)
Open Scope lang_scope.
(**
We begin with a Cbv fixed point combinator for functions with two arguments:
[fix2 f(x)(y).e := λy. (unfold v) v y
where v := fold (λz. (λf.λx.λy. e) (λy. (unfold z) z y))]
This is a version of the combinator given in the LSLR paper adapted for
two argument functions.
(** *** Definitions
We begin with a Cbv fixed point combinator for functions with two arguments:
[fix2 f(x)(y).e := λy. (unfold v) v y
where v := fold (λz. (λf.λx.λy. e) (λy. (unfold z) z y))]
This is a version of the combinator given in the LSLR paper adapted for
two argument functions.
*)
Definition efix2 e :=
let v := efold (λ ((λ λ λ e) @ (λ (eunfold (#1) @ #1 @ #0))))
......
......@@ -4,8 +4,6 @@ Require Import Omega.
Require Import Common.Language Common.Lib.
Require Import BinaryTyped.WeakSubSyntactic BinaryTyped.LogRel BinaryTyped.WeakSub.
(** * Compatibility Lemmas
*)
Lemma eval_step2 {k} (t : typ) {HC : closed k t} η n e1 e2 e2'
(HS : e2 e2') :
E[[ t ]] η n (e1,e2) == E[[ t ]] η n (e1,e2').
......
......@@ -168,7 +168,7 @@ Section Constructions.
clear EQtp; simpl in EQR; clear_dups
end.
(** *** From Semantic to syntactic type variable contexts
(** ** From Semantic to syntactic type variable contexts
Now that we have our semantic notion of a type variable context
([TCRel n], a map from the finite type [Fin.t n] to [T]), we need
......
......@@ -4,7 +4,7 @@ Require Import Common.Language Common.Lib.
Open Scope lang_scope.
(** * Another Binary Logical Relation for Contextual Approximation
(** * Chapter 3. Another binary logical relation
Our third (and final) logical relation will be another LR that is
sound with respect to contextual approximation, but we now want the
......
(** * Language
(** * Chapter 0. Language and common definitions
This file contains the definition of the object language, i.e. the inductive
definitions of types, expressions, values as well as the typing rules and the
......
......@@ -19,7 +19,7 @@ Ltac commute_env ρ :=
rewrite IHρ; simpl_subst_goal; reflexivity
| _ => fail "Can only be used on an environment."
end.
(** ** Substitution lemmas *)
Section EnvSubstsCommute.
Open Scope lang_scope.
......
......@@ -3,14 +3,21 @@ Require Import Common.Language Common.Lib.
Open Scope lang_scope.
(** ** Type checker and interpreter tactics
This file contains several tactic definitions that will be used when
proving logical approximations between terms of the language. They are
meant to be used when the full structure of the term is used - i.e. they
do not contain Coq variables - or the Coq variables they contain are known
to be closed and/or values.
Two stronger versions of the [construction_closed] tactic, to disspell
closedness obligations:
*)
Ltac construction_closed' :=
try construction_closed;
solve [ unfold closed in *; simpl_lift_goal; repeat (f_equal; eauto with shift_closed) ].
(*
Ltac construction_closed' :=
solve [ unfold closed in *; simpl_lift_goal; try (simpl; lift_idx);
repeat (rewrite <- lift_lift); try congruence; eauto with omega construction_closed ].
*)
Ltac construction_closed_inserts :=
repeat match goal with
| [ |- closed _ (insert 0 _ _) ] =>
......@@ -20,6 +27,11 @@ Ltac construction_closed_inserts :=
Create HintDb typings.
(**
A simple type-checking tactic. As the term language does not contain types
and therefore does not admit unique typing, this won't always be enough to
prove any typing obligations.
*)
Ltac check_type_rec :=
simpl_subst_goal;
eauto with typings;
......@@ -30,17 +42,8 @@ Ltac check_type_rec :=
end; try check_type_rec.
Ltac check_type := check_type_rec; construction_closed_inserts.
(*
Ltac check_type :=
repeat (eauto with typings;
match goal with
| [ |- [ _ | _ _ ::: _ ] ] => econstructor
| [ |- context[subst _ _ _] ] => simpl_subst_goal; repeat (rewrite subst_lift)
| [ |- closed _ _ ] => construction_closed_inserts
(* construction_closed_inserts || solve [ inversion_closed; construction_closed_inserts ] *)
| [ |- lookup _ (insert _ _ _) = _ ] => repeat lookup_insert; reflexivity
end).
*)
(** Do a step, depending on the structure of the term. *)
Ltac comp_step :=
match goal with
| [ |- π1 ?e1, ?e2〉↦ _ ] => let v1 := valify e1 in let v2 := valify e2 in
......@@ -73,6 +76,12 @@ Ltac comp_step :=
| [ |- eunfold ?e _ ] => eapply SCunfold; comp_step
end.
(**
This is a counterpart to the [valify] tactic from [Lib.v].
We need to use it sometimes to change values back into expressions
to make some of the matches of [comp_step] go through.
For example, [val_to_exp (vinl v)] does not match [ιl (val_to_exp v)].
*)
Ltac unvalify :=
repeat match goal with
| [ |- context[ val_to_exp ?v ] ] =>
......@@ -88,14 +97,13 @@ Ltac unvalify :=
| vfold ?v1 => change (val_to_exp v) with (efold (val_to_exp v1))
end
end.
(*
Hint Extern 1 =>
match goal with
| [ H: closed 0 ?e |- context[shift 0 ?e] ] => rewrite H
| [ H: closed 0 ?e |- context[subst _ 0 ?e] ] =>
rewrite (closed_subst_invariant 0); [| apply H | omega]
end : substexp.
(**
A tactic that combines [simpl_lift_goal] and [simpl_subst_goal] that
also recognizes that some [lift]s and [subst] have no effect by
checking whether the term in question is closed.
*)
Ltac simpl_subst_lift_goal' :=
autounfold with typings; unvalify; simpl_subst_goal; simpl_lift_goal;
repeat match goal with
......@@ -111,6 +119,12 @@ Ltac simpl_subst_lift_goal :=
| _ => simpl_subst_lift_goal'
end.
(**
Two tactics to prove goals of the form [e1 * e2].
The first one is meant to be used if [e1] and [e2] are known,
the second one should be used if there is a Coq existential variable
in place of [e2].
*)
Ltac comp_min_steps :=
autounfold with typings;
repeat match goal with
......@@ -125,12 +139,3 @@ Ltac comp_max_steps :=
| [ |- mstep _ _ ] => eapply mstep0
end.
(*
Ltac comp_max_steps :=
match goal with
| [ |- mstep _ _ ] =>
simpl; simpl_subst_goal; simpl_lift_goal; eapply mstepS; [comp_step |]; comp_max_steps
| [ |- mstep _ _ ] => solve [simpl; simpl_subst_goal; simpl_lift_goal; eapply mstep0]
| _ => idtac
end.
*)
......@@ -63,7 +63,7 @@ OPT?=
COQDEP?=$(COQBIN)coqdep -c
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQCHKFLAGS?=-silent -o
COQDOCFLAGS?=-interpolate -utf8
COQDOCFLAGS?=-s -interpolate -utf8
COQC?=$(COQBIN)coqc
GALLINA?=$(COQBIN)gallina
COQDOC?=$(COQBIN)coqdoc
......
......@@ -16,7 +16,8 @@ Proof.
intros e e' HS HI; unfold flip in HS; simpl in HS; subst; assumption.
Qed.
(** ** Constructions
(** * Chapter 1. A unary logical relation for type safety
** Constructions
_We now reach the interesting part of the proof: the definition of
the logical relation. As is usual in this type of argument, we
......
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