Commit 083c0c18 authored by POTTIER Francois's avatar POTTIER Francois

Expose new Coq files.

parent 42ddbb4f
Require Import Omega.
Require Import Autosubst.Autosubst.
Require Import MyTactics. (* TEMPORARY *)
(* -------------------------------------------------------------------------- *)
......@@ -167,3 +168,5 @@ Hint Extern 1 (_ = _) => autosubst : autosubst.
metavariables, so the tactic [autosubst] fails. *)
Hint Resolve scons_scomp : autosubst.
(* -------------------------------------------------------------------------- *)
Require Import Omega.
Require Import Autosubst.Autosubst.
Require Import AutosubstExtra. (* just for [upn_ren] *)
Require Import MyTactics. (* TEMPORARY *)
(* This file defines the construction [eos x t], which can be understood as
an end-of-scope mark for [x] in the term [t]. *)
(* It also defines the single-variable substitution t.[u // x], which is the
substitution of [u] for [x] in [t]. *)
(* -------------------------------------------------------------------------- *)
Section EOS.
Context {A} `{Ids A, Rename A, Subst A, SubstLemmas A}.
(* The substitution [Var 0 .: Var 1 .: ... .: Var (x-1) .: Var (x+1) .: ...]
does not have [Var x] in its codomain. Thus, applying this substitution
to a term [t] can be understood as an end-of-scope construct: it means
``end the scope of [x] in [t]''. We write [eos x t] for this construct.
It is also known as [adbmal]: see Hendriks and van Oostrom,
https://doi.org/10.1007/978-3-540-45085-6_11 *)
(* There are at least two ways of defining the above substitution. One way
is to define it in terms of AutoSubst combinators: *)
Definition eos_var x : var -> var :=
(iterate upren x (+1)).
Definition eos x t :=
t.[ren (eos_var x)].
Lemma eos_eq:
forall x t,
t.[upn x (ren (+1))] = eos x t.
Proof.
intros. unfold eos, eos_var. erewrite upn_ren by tc. reflexivity.
Qed.
(* Another way is to define directly as a function of type [var -> var]. *)
Definition lift_var x : var -> var :=
fun y => if le_gt_dec x y then 1 + y else y.
(* The two definitions coincide: *)
Lemma upren_lift_var:
forall x,
upren (lift_var x) = lift_var (S x).
Proof.
intros. f_ext; intros [|y].
{ reflexivity. }
{ simpl. unfold lift_var, var. dblib_by_cases; omega. }
Qed.
Lemma eos_var_eq_lift_var:
eos_var = lift_var.
Proof.
(* An uninteresting proof. *)
f_ext; intros x.
unfold eos_var.
induction x.
{ reflexivity. }
{ rewrite iterate_S.
rewrite IHx.
rewrite upren_lift_var.
reflexivity. }
Qed.
(* -------------------------------------------------------------------------- *)
(* [eos] enjoys certain commutation laws. *)
(* Ending the scope of variable [k], then the scope of variable [s], is the
same as first ending the scope of variable [1 + s], then ending the scope
of variable [k]. This holds provided [k <= s] is true, i.e., [k] is the
most recently-introduced variable.*)
Lemma lift_var_lift_var:
forall k s,
k <= s ->
lift_var s >>> lift_var k = lift_var k >>> lift_var (S s).
Proof.
(* By case analysis. *)
intros. f_ext; intros x. asimpl.
unfold lift_var, var. dblib_by_cases; omega.
Qed.
Lemma eos_eos:
forall k s t,
k <= s ->
eos k (eos s t) = eos (1 + s) (eos k t).
Proof.
intros. unfold eos. asimpl.
rewrite eos_var_eq_lift_var.
rewrite lift_var_lift_var by eauto.
reflexivity.
Qed.
(* What about the case where [k] is the least recently-introduced variable?
It is obtained by symmetry, of course. *)
Lemma eos_eos_reversed:
forall k s t,
k >= s + 1 ->
eos k (eos s t) = eos s (eos (k - 1) t).
Proof.
intros.
replace k with (1 + (k - 1)) by omega.
rewrite <- eos_eos by omega.
replace (1 + (k - 1) - 1) with (k - 1) by omega.
reflexivity.
Qed.
(* -------------------------------------------------------------------------- *)
(* Single-variable substitutions. *)
(* [subst_var u x] is the substitution of [u] for [x]. *)
(* We give a direct definition of it as a function of type [var -> term],
defined by cases. I don't know if it could also be nicely defined in
terms of the basic combinators of de Bruijn algebra. Note that the
candidate definition [upn x (t .: ids)] is WRONG when [x > 0]. *)
Definition subst_var (u : A) (x y : var) : A :=
match lt_eq_lt_dec y x with
| inleft (left _) => ids y
| inleft (right _) => u
| inright _ => ids (y - 1)
end.
(* A nice notation: [t.[u // x]] is the substitution of [u] for [x] in [t]. *)
Notation "t .[ u // x ]" := (subst (subst_var u x) t)
(at level 2, u at level 200, left associativity,
format "t .[ u // x ]") : subst_scope.
(* The following laws serve as sanity checks: we got the definition right. *)
Lemma subst_var_miss_1:
forall x y u,
y < x ->
(ids y).[u // x] = ids y.
Proof.
intros. asimpl. unfold subst_var. dblib_by_cases. reflexivity.
Qed.
Lemma subst_var_match:
forall x u,
(ids x).[ u // x ] = u.
Proof.
intros. asimpl. unfold subst_var. dblib_by_cases. reflexivity.
Qed.
Lemma subst_var_miss_2:
forall x y u,
x < y ->
(ids y).[u // x] = ids (y - 1).
Proof.
intros. asimpl. unfold subst_var. dblib_by_cases. reflexivity.
Qed.
(* In the special case where [x] is 0, the substitution [t // 0] can also
be written [t/], which is an AutoSubst notation for [t .: ids]. *)
Lemma subst_var_0:
forall t u,
t.[u // 0] = t.[u/].
Proof.
intros. f_equal. clear t.
f_ext. intros [|x].
{ reflexivity. }
{ unfold subst_var. simpl. f_equal. omega. }
Qed.
(* -------------------------------------------------------------------------- *)
(* A cancellation law: substituting for a variable [x] that does not occur in
[t] yields just [t]. In other words, a substitution for [x] vanishes when
it reaches [eos x _]. *)
(* In informal syntax, this lemma would be written:
t[u/x] = t
under the hypothesis that x does not occur free in t.
In de Bruijn style, the statement is just as short, and does not have a
side condition. Instead, it requires an explicit [eos x _] to appear at the
root of the term to which the substitution is applied; this may require
rewriting before this lemma can be applied. *)
Lemma subst_eos:
forall x t u,
(eos x t).[u // x] = t.
Proof.
intros.
(* Again, let's simplify this first. *)
unfold eos. asimpl.
(* Aha! We can forget about [t], and focus on proving that two
substitutions are equal. To do so, it is sufficient that
their actions on a variable [y] are the same. *)
rewrite <- subst_id.
f_equal. clear t.
f_ext. intro y.
(* The proof is easy if we replace [eos_var] with [lift_var]. *)
rewrite eos_var_eq_lift_var. simpl.
unfold subst_var, lift_var. dblib_by_cases; f_equal; omega.
Qed.
(* The above property allows us to prove that [eos x _] is injective.
Indeed, it has an inverse, namely [u // x], where [u] is arbitrary. *)
Lemma eos_injective:
forall x t1 t2,
eos x t1 = eos x t2 ->
t1 = t2.
Proof.
intros.
pose (u := t1). (* dummy *)
erewrite <- (subst_eos x t1 u).
erewrite <- (subst_eos x t2 u).
congruence.
Qed.
(* -------------------------------------------------------------------------- *)
(* More commutation laws. *)
Lemma eos_subst_1:
forall k s t u,
k <= s ->
eos k (t.[u // s]) = (eos k t).[eos k u // s + 1].
Proof.
intros. unfold eos. asimpl. f_equal. clear t.
rewrite eos_var_eq_lift_var.
f_ext. intros y.
asimpl.
unfold subst_var, lift_var.
dblib_by_cases; asimpl; dblib_by_cases; solve [ eauto | f_equal; omega ].
Qed.
Lemma eos_subst_2:
forall k s t u,
s <= k ->
eos k (t.[u // s]) = (eos (k + 1) t).[eos k u // s].
Proof.
intros. unfold eos. asimpl. f_equal. clear t.
rewrite eos_var_eq_lift_var.
f_ext. intros y.
asimpl.
unfold subst_var, lift_var.
dblib_by_cases; asimpl; dblib_by_cases; solve [ eauto | f_equal; omega ].
Qed.
Lemma subst_subst:
forall t k v s w,
k <= s ->
t.[w // k].[v // s] =
t.[eos k v // 1 + s].[w.[v // s] // k].
Proof.
(* First, get rid of [t]. It is sufficient to consider the action of
these substitutions at a variable [y]. *)
intros. asimpl. f_equal. clear t. f_ext. intros y.
(* Replace [eos_var] with [lift_var], whose definition is more direct. *)
unfold eos. rewrite eos_var_eq_lift_var.
(* Then, use brute force (case analysis) to prove that the goal holds. *)
unfold subst_var. simpl.
dblib_by_cases; asimpl; dblib_by_cases;
(* This case analysis yields 5 cases, of which 4 are trivial... *)
eauto.
(* ... thus, one case remains. *)
(* Now get rid of [v]. It is again sufficient to consider the action
of these substitutions at a variable [z]. *)
replace v with v.[ids] at 1 by autosubst.
f_equal. f_ext. intros z. simpl.
(* Again, use brute force. *)
unfold lift_var. dblib_by_cases; f_equal. unfold var. omega.
(* Not really proud of this proof. *)
Qed.
Lemma pun_1:
forall t x,
(eos x t).[ ids x // x + 1 ] = t.
Proof.
(* First, get rid of [t]. It is sufficient to consider the action of
these substitutions at a variable [y]. *)
intros. unfold eos. asimpl.
replace t with t.[ids] at 2 by autosubst.
f_equal. clear t. f_ext. intros y.
(* Replace [eos_var] with [lift_var], whose definition is more direct. *)
rewrite eos_var_eq_lift_var.
(* Then, use brute force (case analysis) to prove that the goal holds. *)
simpl. unfold subst_var, lift_var. dblib_by_cases; f_equal; unfold var; omega.
Qed.
Lemma pun_2:
forall t x,
(eos (x + 1) t).[ ids x // x ] = t.
Proof.
(* First, get rid of [t]. It is sufficient to consider the action of
these substitutions at a variable [y]. *)
intros. unfold eos. asimpl.
replace t with t.[ids] at 2 by autosubst.
f_equal. clear t. f_ext. intros y.
(* Replace [eos_var] with [lift_var], whose definition is more direct. *)
rewrite eos_var_eq_lift_var.
(* Then, use brute force (case analysis) to prove that the goal holds. *)
simpl. unfold subst_var, lift_var. dblib_by_cases; f_equal; unfold var; omega.
Qed.
End EOS.
(* Any notations defined in the above section must now be repeated. *)
Notation "t .[ u // x ]" := (subst (subst_var u x) t)
(at level 2, u at level 200, left associativity,
format "t .[ u // x ]") : subst_scope.
(* The tactic [subst_var] attempts to simplify applications of [subst_var]. *)
Ltac subst_var :=
first [
rewrite subst_var_miss_1 by omega
| rewrite subst_var_match by omega
| rewrite subst_var_miss_2 by omega
].
Require Import List.
Require Import MyTactics. (* TEMPORARY *)
Require Import Autosubst.Autosubst.
Require Import Autosubst_EOS. (* [eos_var] *)
(* Environments are sometimes represented as finite lists. This file
provides a few notions that helps deal with this representation. *)
Section Env.
Context {A} `{Ids A, Rename A, Subst A, SubstLemmas A}.
(* -------------------------------------------------------------------------- *)
(* The function [env2subst default], where [default] is a default value,
converts an environment (a finite list) to a substitution (a total
function). *)
Definition env2subst (default : A) (e : list A) (x : var) : A :=
nth x e default.
(* -------------------------------------------------------------------------- *)
(* [env_ren_comp e xi e'] means (roughly) that the environment [e] is equal to
the composition of the renaming [xi] and the environment [e'], that is,
[e = xi >>> e']. We also explicitly require the environments [e] and [e']
to have matching lengths, up to [xi], as this is *not* a consequence of
the other premise. *)
Inductive env_ren_comp : list A -> (var -> var) -> list A -> Prop :=
| EnvRenComp:
forall e xi e',
(forall x, x < length e -> xi x < length e') ->
(forall x default, nth x e default = nth (xi x) e' default) ->
env_ren_comp e xi e'.
(* A reformulation of the second premise in the above definition. *)
Lemma env_ren_comp_eq:
forall e xi e',
(forall default, env2subst default e = xi >>> env2subst default e') <->
(forall x default, nth x e default = nth (xi x) e' default).
Proof.
unfold env2subst. split; intros h; intros.
{ change (nth x e default) with ((fun x => nth x e default) x).
rewrite h. reflexivity. }
{ f_ext; intro x. eauto. }
Qed.
(* -------------------------------------------------------------------------- *)
(* Initialization: [e = id >>> e]. *)
Lemma env_ren_comp_id:
forall e,
env_ren_comp e (fun x => x) e.
Proof.
econstructor; eauto.
Qed.
(* -------------------------------------------------------------------------- *)
(* The relation [e = xi >>> e'] can be taken under a binder, as follows. *)
Lemma env_ren_comp_up:
forall e xi e' v,
env_ren_comp e xi e' ->
env_ren_comp (v :: e) (upren xi) (v :: e').
Proof.
inversion 1; intros; subst; econstructor;
intros [|x]; intros; simpl in *; eauto with omega.
Qed.
(* -------------------------------------------------------------------------- *)
(* One element can be prepended to [e'], provided [xi] is adjusted. *)
Lemma env_ren_comp_prepend:
forall e xi e' v,
env_ren_comp e xi e' ->
env_ren_comp e (xi >>> (+1)) (v :: e').
Proof.
inversion 1; intros; subst.
econstructor; intros; simpl; eauto with omega.
Qed.
(* -------------------------------------------------------------------------- *)
(* A consequence of [env_ren_comp_id] and [env_ren_comp_prepend]. The renaming
(+1) will eat away the first entry in [v :: e]. *)
Lemma env_ren_comp_plus1:
forall e v,
env_ren_comp e (+1) (v :: e).
Proof.
econstructor; intros; simpl; eauto with omega.
Qed.
(* -------------------------------------------------------------------------- *)
(* More generally, the renaming [eos_var x], which means that [x] goes out of
scope, will eat away the entry at index [x] in [e1 ++ v :: e2]. *)
Lemma env_ren_comp_eos_var:
forall x e1 v e2,
x = length e1 ->
env_ren_comp (e1 ++ e2) (eos_var x) (e1 ++ v :: e2).
Proof.
rewrite eos_var_eq_lift_var. unfold lift_var.
econstructor; intros y; dblib_by_cases.
{ rewrite app_length in *. simpl. omega. }
{ rewrite app_length in *. simpl. omega. }
{ do 2 (rewrite app_nth2 by omega).
replace (1 + y - length e1) with (1 + (y - length e1)) by omega.
reflexivity. }
{ do 2 (rewrite app_nth1 by omega).
reflexivity. }
Qed.
(* -------------------------------------------------------------------------- *)
End Env.
Hint Resolve
env_ren_comp_id
env_ren_comp_up
env_ren_comp_prepend
env_ren_comp_plus1
env_ren_comp_eos_var
: env_ren_comp.
Require Import Omega.
Require Import Autosubst.Autosubst.
Require Import AutosubstExtra.
Require Import Autosubst_EOS.
(* -------------------------------------------------------------------------- *)
Class IdsLemmas (term : Type) {Ids_term : Ids term} := {
(* The identity substitution is injective. *)
ids_inj:
forall x y,
ids x = ids y ->
x = y
}.
(* -------------------------------------------------------------------------- *)
Section FreeVars.
Context
{A : Type}
{Ids_A : Ids A}
{Rename_A : Rename A}
{Subst_A : Subst A}
{IdsLemmas_A : IdsLemmas A}
{SubstLemmas_A : SubstLemmas A}.
(* -------------------------------------------------------------------------- *)
(* A reformulation of [ids_inj]. *)
Lemma ids_inj_False:
forall x y,
ids x = ids y ->
x <> y ->
False.
Proof.
intros.
assert (x = y). { eauto using ids_inj. }
unfold var in *.
omega.
Qed.
(* -------------------------------------------------------------------------- *)
(* The predicate [fv k t] means that the free variables of the term [t] are
contained in the semi-open interval [0..k). *)
Definition fv k t :=
t.[upn k (ren (+1))] = t.
(* -------------------------------------------------------------------------- *)
(* The predicate [closed t] means that the term [t] is closed, that is, [t]
has no free variables. *)
Definition closed :=
fv 0.
(* -------------------------------------------------------------------------- *)
(* This technical lemma states that the renaming [+1] is injective. *)
Lemma lift_inj_ids:
forall t x,
t.[ren (+1)] = ids (S x) <-> t = ids x.
Proof.
split; intros.
{ eapply lift_inj. autosubst. }
{ subst. autosubst. }
Qed.
(* -------------------------------------------------------------------------- *)
(* This lemma characterizes the meaning of [fv k] when applied to a variable. *)
Lemma fv_ids_eq:
forall k x,
fv k (ids x) <-> x < k.
Proof.
unfold fv. induction k; intros.
(* Base case. *)
{ asimpl. split; intros; elimtype False.
{ eauto using ids_inj_False. }
{ omega. }
}
(* Step. *)
{ destruct x; asimpl.
{ split; intros. { omega. } { reflexivity. } }
{ rewrite lift_inj_ids.
rewrite <- id_subst.
rewrite IHk. omega. }
}
Qed.
(* -------------------------------------------------------------------------- *)
(* A simplification lemma. *)
Lemma fv_lift:
forall k i t,
fv (k + i) t.[ren (+i)] <-> fv k t.
Proof.
unfold fv. intros. asimpl.
rewrite Nat.add_comm.
rewrite <- upn_upn.
erewrite plus_upn by eauto.
rewrite <- subst_comp.
split; intros.
{ eauto using lift_injn. }
{ f_equal. eauto. }
Qed.
(* -------------------------------------------------------------------------- *)
(* If [t] has at most [n - 1] free variables,
and if [x] is inserted among them,
then we get [eos x t],
which has at most [n] free variables. *)
Lemma fv_eos:
forall x n t,
x < n ->
fv (n - 1) t ->
fv n (eos x t).
Proof.