Library ConfluencebyZofGeneralisedLocalDeBruijninRocq
- email address: vvo@sussex.ac.uk.
- developed on macOS Tahoe.
- code updated from Coq 8.16.1 to Rocq 9.2.0.
- dependence on SSReflect removed (extraction to Haskell failed for old coq code in new rocq).
- demo code showcasing the construction of valleys given (simple) peaks added
exs and sub
(vO & van der Looij & Zwitserlood, ALPS 2004).
lift_rec and subst_rec there, on ordinary
De Bruijn terms (and multisteps), that is on generalised
local De Bruijn terms where the end-of-scopes occur only
on top of the variable (only var may have a
non-zero number of end-of-scopes).
- to extract Haskell confluence function
- From Stdlib Require Import Extraction.
From Corelib Require Extraction.
- enable ssreflect tactics
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
- scopes as unary natural numbers
Require Import Nat.
- automatic scope comparisons via lia
From Stdlib Require Import Psatz.
- move between bool and Prop for equality and comparison of scopes / nats
From Stdlib Require Import PeanoNat.
From Stdlib Require Import Arith.Compare_dec.
From Stdlib Require Import Arith.Compare_dec.
- using x_equation coming from Function x to avoid (some) boiler plate code
From Stdlib Require FunInd.
objects of rewrite system: generalised local De Bruijn terms, with operations for beta
and bullet function for Z
Section ConfluencebyZ.
Inductive lam :=
| var : nat -> lam
| abs : nat -> lam -> lam
| app : nat -> lam -> lam -> lam.
Function eos (t : lam) : nat :=
match t with
| var i => i
| abs i _ => i
| app i _ _ => i
end.
Function dcs (t:lam) : lam :=
match t with
| var i => var (i-1)
| abs i s => abs (i-1) s
| app i s u => app (i-1) s u
end.
Function ads (n:nat) (t:lam) : lam :=
match t with
| var i => var (i+n)
| abs i s => abs (i+n) s
| app i s u => app (i+n) s u
end.
Inductive lam :=
| var : nat -> lam
| abs : nat -> lam -> lam
| app : nat -> lam -> lam -> lam.
Function eos (t : lam) : nat :=
match t with
| var i => i
| abs i _ => i
| app i _ _ => i
end.
Function dcs (t:lam) : lam :=
match t with
| var i => var (i-1)
| abs i s => abs (i-1) s
| app i s u => app (i-1) s u
end.
Function ads (n:nat) (t:lam) : lam :=
match t with
| var i => var (i+n)
| abs i s => abs (i+n) s
| app i s u => app (i+n) s u
end.
extrusion and substitution as in vO & vdL & Z 2004
Fixpoint exs1 (t:lam)(d:nat){struct t} : lam :=
if d <=? (eos t) then ads 1 t else
match t with
| var i => var i
| abs i s => abs i (exs1 s (S (d - (eos t))))
| app i s u => app i (exs1 s (d - (eos t))) (exs1 u (d - (eos t)))
end.
Function exs (n:nat)(d:nat)(t:lam) : lam :=
match n with
| 0 => t
| S m => exs m d (exs1 t d)
end.
Function sub (d:nat)(t:lam) (s:lam) : lam :=
let j := eos t in if j <=? d then let e := d - j in match t with
| var i => if j =? d then ads i s else t
| abs i u => abs i (sub (S e) u s)
| app i u v => app i (sub e u s) (sub e v s)
end else dcs t.
Definition beta (n:nat) (t s:lam) :=
sub 0 (exs n 1 t) s.
if d <=? (eos t) then ads 1 t else
match t with
| var i => var i
| abs i s => abs i (exs1 s (S (d - (eos t))))
| app i s u => app i (exs1 s (d - (eos t))) (exs1 u (d - (eos t)))
end.
Function exs (n:nat)(d:nat)(t:lam) : lam :=
match n with
| 0 => t
| S m => exs m d (exs1 t d)
end.
Function sub (d:nat)(t:lam) (s:lam) : lam :=
let j := eos t in if j <=? d then let e := d - j in match t with
| var i => if j =? d then ads i s else t
| abs i u => abs i (sub (S e) u s)
| app i u v => app i (sub e u s) (sub e v s)
end else dcs t.
Definition beta (n:nat) (t s:lam) :=
sub 0 (exs n 1 t) s.
bullet a la Loader, LFCS University of Edinburgh 1997
Function bul (t : lam) : lam :=
match t with
| app i (abs j s) u => ads i (beta j (bul s) (bul u))
| var i => var i
| abs i s => abs i (bul s)
| app i s u => app i (bul s) (bul u)
end.
match t with
| app i (abs j s) u => ads i (beta j (bul s) (bul u))
| var i => var i
| abs i s => abs i (bul s)
| app i s u => app i (bul s) (bul u)
end.
interaction between operations as conditional rewrite rules.
conditions on end-of-scopes as constraints on nats
Lemma eosads : forall (n:nat)(t:lam), eos (ads n t) = eos(t) + n.
intros n t. case t; intuition. Qed.
Lemma eosexs1 : forall (t:lam)(d e:nat), e <= eos t -> e <= eos (exs1 t d).
intros t d; case t; simpl; intros m; case (d <=? m); simpl; lia. Qed.
Lemma eosexs : forall (n:nat)(t:lam)(d e:nat), e <= eos t -> e <= eos (exs n d t).
induction n; intros t d e H; [| rewrite exs_equation; apply IHn ; apply eosexs1]; auto. Qed.
Lemma eosbul : forall (t:lam)(n:nat), n <= eos t -> n <= eos (bul t).
intro t; case t; [auto|auto|].
intros n l; case l; [auto | intros i u v j;simpl;rewrite eosads;lia | auto]. Qed.
Ltac eqs :=
try (apply eosbul; try eqs);
try (apply eosexs; try eqs);
try (apply eosexs1; try eqs);
try rewrite eosads;
trivial;
try lia;
try (f_equal; lia);
try (f_equal;f_equal;lia);
try simpl in *;
f_equal;f_equal;f_equal;lia.
intros n t. case t; intuition. Qed.
Lemma eosexs1 : forall (t:lam)(d e:nat), e <= eos t -> e <= eos (exs1 t d).
intros t d; case t; simpl; intros m; case (d <=? m); simpl; lia. Qed.
Lemma eosexs : forall (n:nat)(t:lam)(d e:nat), e <= eos t -> e <= eos (exs n d t).
induction n; intros t d e H; [| rewrite exs_equation; apply IHn ; apply eosexs1]; auto. Qed.
Lemma eosbul : forall (t:lam)(n:nat), n <= eos t -> n <= eos (bul t).
intro t; case t; [auto|auto|].
intros n l; case l; [auto | intros i u v j;simpl;rewrite eosads;lia | auto]. Qed.
Ltac eqs :=
try (apply eosbul; try eqs);
try (apply eosexs; try eqs);
try (apply eosexs1; try eqs);
try rewrite eosads;
trivial;
try lia;
try (f_equal; lia);
try (f_equal;f_equal;lia);
try simpl in *;
f_equal;f_equal;f_equal;lia.
preliminary rewrite rules on interaction (should be automatable)
Lemma dcsvar : forall (i: nat), dcs (var i) = var (i-1). auto. Qed.
Lemma dcsabs : forall (i: nat)(t:lam), dcs (abs i t) = abs (i-1) t. auto. Qed.
Lemma dcsapp : forall (i: nat)(t s:lam), dcs (app i t s) = app (i-1) t s. auto. Qed.
Lemma dcsadsn : forall (n:nat)(t:lam), n > 0 -> dcs (ads n t) = ads (n-1) t.
intros n t. case t; simpl; intros; eqs. Qed.
Lemma dcsadst : forall (t:lam)(n:nat), eos t > 0 -> dcs (ads n t) = ads n (dcs t).
intros t n. case t; simpl; intros; eqs. Qed.
Lemma adsvar : forall (n i: nat), ads n (var i) = var (i+n). auto. Qed.
Lemma adsabs : forall (n i: nat)(t:lam), ads n (abs i t) = abs (i+n) t. auto. Qed.
Lemma adsapp : forall (n i: nat)(t s:lam), ads n (app i t s) = app (i+n) t s. auto. Qed.
Lemma adszer : forall (t:lam)(n:nat), n = 0 -> ads n t = t.
intro t. case t; intros ; subst; eqs. Qed.
Lemma adsads : forall (n m:nat)(t:lam),
ads m (ads n t) = ads (n+m) t.
intros n m t. case t;intros; simpl; f_equal; lia. Qed.
Lemma exs1_equation : forall (t : lam) (d : nat), exs1 t d =
if d <=? eos t then ads 1 t else
match t with
| var i => var i
| abs i s => abs i (exs1 s (S (d - eos t)))
| app i s u => app i (exs1 s (d - eos t)) (exs1 u (d - eos t))
end.
intro t. case t; intuition. Qed.
Lemma exsle : forall (n d:nat)(t:lam), d <= eos t ->
exs n d t = ads n t.
induction n; intros d t H; rewrite exs_equation.
+ rewrite adszer; trivial.
+ rewrite IHn;[rewrite exs1_equation; rewrite leb_correct; try rewrite adsads | apply eosexs1]; trivial.
Qed.
Lemma exslevar : forall (n d:nat)(i:nat), d <= i -> exs n d (var i) = var (i+n).
intros. rewrite exsle; auto. Qed.
Lemma exsleabs : forall (n d:nat)(i:nat)(t:lam), d <= i -> exs n d (abs i t) = abs (i+n) t.
intros. rewrite exsle; auto. Qed.
Lemma exsleapp : forall (n d:nat)(i:nat)(t s:lam), d <= i -> exs n d (app i t s) = app (i+n) t s.
intros. rewrite exsle; auto. Qed.
Lemma exsleads : forall (n d:nat)(i:nat)(t:lam), d <= i -> exs n d (ads i t) = ads (i+n) t.
intros. rewrite exsle; try eqs; rewrite adsads; trivial. Qed.
Lemma exsgt : forall (n d:nat)(t:lam), ~d <= eos t ->
exs n d t = match t with
| (var i) => var i
| (abs i t) => abs i (exs n (S (d-i)) t)
| (app i t s) => app i (exs n (d-i) t) (exs n (d-i) s)
end.
induction n; intros d t H; rewrite exs_equation.
+ case t; trivial.
+ rewrite exs1_equation. rewrite leb_correct_conv; try lia.
revert H. case t; intros; (rewrite IHn; simpl in *; [trivial | f_equal]);trivial.
Qed.
Lemma exsgtvar : forall (n d:nat)(i:nat), ~d <= i -> exs n d (var i) = var i.
intros. rewrite exsgt; auto. Qed.
Lemma exsgtabs : forall (n d:nat)(i:nat)(t:lam), ~d <= i -> exs n d (abs i t) =
abs i (exs n (S (d-i)) t).
intros. rewrite exsgt; auto. Qed.
Lemma exsgtapp : forall (n d:nat)(i:nat)(t s:lam), ~d <= i -> exs n d (app i t s) =
app i (exs n (d-i) t) (exs n (d-i) s).
intros. rewrite exsgt; auto. Qed.
Lemma sublt : forall (t:lam)(d:nat)(s:lam), d < eos t ->
sub d t s = dcs t.
intros t d s. case t;simpl;intros; rewrite leb_correct_conv; trivial. Qed.
Lemma subgtvar : forall (j d:nat)(s:lam), j < d ->
sub d (var j) s = (var j).
intros j d s H; simpl; rewrite leb_correct; try lia.
cut ((j =? d) = false).
intro R; rewrite R; trivial.
apply Nat.eqb_neq; lia. Qed.
Lemma subeqvar : forall (j d:nat)(s:lam), j = d ->
sub d (var j) s = ads j s.
intros; simpl; rewrite leb_correct; [subst; rewrite Nat.eqb_refl; trivial | lia]. Qed.
Lemma subgeabs : forall (j d:nat)(t s:lam), j <= d ->
sub d (abs j t) s = abs j (sub (S (d-j)) t s).
intros; simpl; rewrite leb_correct; [trivial | lia]. Qed.
Lemma subgeapp : forall (j d:nat)(t u s:lam), j <= d ->
sub d (app j t u) s = app j (sub (d-j) t s) (sub (d-j) u s).
intros. simpl. rewrite leb_correct; [ trivial | lia]. Qed.
Lemma bulbet : forall (i j:nat)(s u:lam), bul (app i (abs j s) u) =
ads i (beta j (bul s) (bul u)). auto. Qed.
Lemma bulvar : forall (i:nat), bul (var i) = var i. auto. Qed.
Lemma bulabs : forall (i:nat)(s:lam), bul (abs i s) = abs i (bul s). auto. Qed.
Lemma bulappvar : forall (i j:nat)(u:lam), bul (app i (var j) u) =
app i (var j) (bul u). auto. Qed.
Lemma bulappapp : forall (i j:nat)(s u v:lam), bul (app i (app j s v) u) =
app i (bul (app j s v)) (bul u). auto. Qed.
Create Rewrite HintDb gldb.
Hint Rewrite dcsvar dcsabs dcsapp
adsvar adsabs adsapp adsads
bulbet bulvar bulabs bulappvar bulappapp : gldb.
Hint Rewrite adszer dcsadsn dcsadst
exslevar exsleabs exsleapp exsleads exsgtvar exsgtabs exsgtapp exsle
sublt subgtvar subeqvar subgeabs subgeapp using eqs : gldb.
Ltac nf := autorewrite with gldb in *; try eqs.
Lemma subgeads : forall (t:lam)(i k:nat), i <= k -> forall (s:lam),
sub k (ads i t) s = ads i (sub (k-i) t s).
intros t i k. destruct (le_dec (i+(eos t)) k) as [Hle | Hgt ].
revert Hle. case t; intro n; intros; [ destruct (Nat.eq_dec (i+n) k) | |]; nf.
intros; nf.
Qed.
Lemma dcsabs : forall (i: nat)(t:lam), dcs (abs i t) = abs (i-1) t. auto. Qed.
Lemma dcsapp : forall (i: nat)(t s:lam), dcs (app i t s) = app (i-1) t s. auto. Qed.
Lemma dcsadsn : forall (n:nat)(t:lam), n > 0 -> dcs (ads n t) = ads (n-1) t.
intros n t. case t; simpl; intros; eqs. Qed.
Lemma dcsadst : forall (t:lam)(n:nat), eos t > 0 -> dcs (ads n t) = ads n (dcs t).
intros t n. case t; simpl; intros; eqs. Qed.
Lemma adsvar : forall (n i: nat), ads n (var i) = var (i+n). auto. Qed.
Lemma adsabs : forall (n i: nat)(t:lam), ads n (abs i t) = abs (i+n) t. auto. Qed.
Lemma adsapp : forall (n i: nat)(t s:lam), ads n (app i t s) = app (i+n) t s. auto. Qed.
Lemma adszer : forall (t:lam)(n:nat), n = 0 -> ads n t = t.
intro t. case t; intros ; subst; eqs. Qed.
Lemma adsads : forall (n m:nat)(t:lam),
ads m (ads n t) = ads (n+m) t.
intros n m t. case t;intros; simpl; f_equal; lia. Qed.
Lemma exs1_equation : forall (t : lam) (d : nat), exs1 t d =
if d <=? eos t then ads 1 t else
match t with
| var i => var i
| abs i s => abs i (exs1 s (S (d - eos t)))
| app i s u => app i (exs1 s (d - eos t)) (exs1 u (d - eos t))
end.
intro t. case t; intuition. Qed.
Lemma exsle : forall (n d:nat)(t:lam), d <= eos t ->
exs n d t = ads n t.
induction n; intros d t H; rewrite exs_equation.
+ rewrite adszer; trivial.
+ rewrite IHn;[rewrite exs1_equation; rewrite leb_correct; try rewrite adsads | apply eosexs1]; trivial.
Qed.
Lemma exslevar : forall (n d:nat)(i:nat), d <= i -> exs n d (var i) = var (i+n).
intros. rewrite exsle; auto. Qed.
Lemma exsleabs : forall (n d:nat)(i:nat)(t:lam), d <= i -> exs n d (abs i t) = abs (i+n) t.
intros. rewrite exsle; auto. Qed.
Lemma exsleapp : forall (n d:nat)(i:nat)(t s:lam), d <= i -> exs n d (app i t s) = app (i+n) t s.
intros. rewrite exsle; auto. Qed.
Lemma exsleads : forall (n d:nat)(i:nat)(t:lam), d <= i -> exs n d (ads i t) = ads (i+n) t.
intros. rewrite exsle; try eqs; rewrite adsads; trivial. Qed.
Lemma exsgt : forall (n d:nat)(t:lam), ~d <= eos t ->
exs n d t = match t with
| (var i) => var i
| (abs i t) => abs i (exs n (S (d-i)) t)
| (app i t s) => app i (exs n (d-i) t) (exs n (d-i) s)
end.
induction n; intros d t H; rewrite exs_equation.
+ case t; trivial.
+ rewrite exs1_equation. rewrite leb_correct_conv; try lia.
revert H. case t; intros; (rewrite IHn; simpl in *; [trivial | f_equal]);trivial.
Qed.
Lemma exsgtvar : forall (n d:nat)(i:nat), ~d <= i -> exs n d (var i) = var i.
intros. rewrite exsgt; auto. Qed.
Lemma exsgtabs : forall (n d:nat)(i:nat)(t:lam), ~d <= i -> exs n d (abs i t) =
abs i (exs n (S (d-i)) t).
intros. rewrite exsgt; auto. Qed.
Lemma exsgtapp : forall (n d:nat)(i:nat)(t s:lam), ~d <= i -> exs n d (app i t s) =
app i (exs n (d-i) t) (exs n (d-i) s).
intros. rewrite exsgt; auto. Qed.
Lemma sublt : forall (t:lam)(d:nat)(s:lam), d < eos t ->
sub d t s = dcs t.
intros t d s. case t;simpl;intros; rewrite leb_correct_conv; trivial. Qed.
Lemma subgtvar : forall (j d:nat)(s:lam), j < d ->
sub d (var j) s = (var j).
intros j d s H; simpl; rewrite leb_correct; try lia.
cut ((j =? d) = false).
intro R; rewrite R; trivial.
apply Nat.eqb_neq; lia. Qed.
Lemma subeqvar : forall (j d:nat)(s:lam), j = d ->
sub d (var j) s = ads j s.
intros; simpl; rewrite leb_correct; [subst; rewrite Nat.eqb_refl; trivial | lia]. Qed.
Lemma subgeabs : forall (j d:nat)(t s:lam), j <= d ->
sub d (abs j t) s = abs j (sub (S (d-j)) t s).
intros; simpl; rewrite leb_correct; [trivial | lia]. Qed.
Lemma subgeapp : forall (j d:nat)(t u s:lam), j <= d ->
sub d (app j t u) s = app j (sub (d-j) t s) (sub (d-j) u s).
intros. simpl. rewrite leb_correct; [ trivial | lia]. Qed.
Lemma bulbet : forall (i j:nat)(s u:lam), bul (app i (abs j s) u) =
ads i (beta j (bul s) (bul u)). auto. Qed.
Lemma bulvar : forall (i:nat), bul (var i) = var i. auto. Qed.
Lemma bulabs : forall (i:nat)(s:lam), bul (abs i s) = abs i (bul s). auto. Qed.
Lemma bulappvar : forall (i j:nat)(u:lam), bul (app i (var j) u) =
app i (var j) (bul u). auto. Qed.
Lemma bulappapp : forall (i j:nat)(s u v:lam), bul (app i (app j s v) u) =
app i (bul (app j s v)) (bul u). auto. Qed.
Create Rewrite HintDb gldb.
Hint Rewrite dcsvar dcsabs dcsapp
adsvar adsabs adsapp adsads
bulbet bulvar bulabs bulappvar bulappapp : gldb.
Hint Rewrite adszer dcsadsn dcsadst
exslevar exsleabs exsleapp exsleads exsgtvar exsgtabs exsgtapp exsle
sublt subgtvar subeqvar subgeabs subgeapp using eqs : gldb.
Ltac nf := autorewrite with gldb in *; try eqs.
Lemma subgeads : forall (t:lam)(i k:nat), i <= k -> forall (s:lam),
sub k (ads i t) s = ads i (sub (k-i) t s).
intros t i k. destruct (le_dec (i+(eos t)) k) as [Hle | Hgt ].
revert Hle. case t; intro n; intros; [ destruct (Nat.eq_dec (i+n) k) | |]; nf.
intros; nf.
Qed.
main rewrite rules on interaction
Lemma dcsexs : forall (t: lam)(d n:nat), d > 0 -> 0 < eos t ->
dcs (exs n d t) = exs n (d-1) (dcs t).
intros t d n Hd.
case t; intro i; case i; intros; simpl in * |-; try lia; elim (le_dec d (S n0)); intros; nf. Qed.
Lemma exsads : forall (t:lam)(i d k:nat), ~(d <= i) ->
exs k d (ads i t) = ads i (exs k (d-i) t).
intros t i d k Hd. elim (le_dec (d-i) (eos t)); case t; intros; nf. Qed.
Lemma dcsbul : forall (t:lam), eos t > 0 ->
dcs (bul t) = bul (dcs t).
intro t. case t; [ | | intros n u; case u]; intros; nf. Qed.
Lemma bulads : forall (t:lam)(n:nat),
bul (ads n t) = ads n (bul t).
intro t. case t; [ | | intros n u; case u]; intros; nf. Qed.
Hint Rewrite dcsexs exsads subgeads dcsbul using eqs : gldb.
Hint Rewrite <- bulads : gldb.
Lemma exsbelowexs : forall (t:lam)(e d k m:nat), d < e ->
exs m d (exs k e t) = exs k (e+m) (exs m d t).
intro t. elim t; [ intro i | intros i s IHs | intros i s IHs u IHu ]; intros e d k m H;
(destruct (le_dec d i); [ destruct (le_dec e i) |]; nf); f_equal;
[ rewrite IHs | rewrite IHs | rewrite IHu] ; eqs.
Qed.
Lemma exsinexs : forall (e:nat)(t:lam)(d k m:nat), e <= m ->
exs (k+m) d t = exs k (d+e) (exs m d t).
intros e t;elim t;[ intro i | intros i s IHs | intros i s IHs u IHu ]; intros d k m H;
(destruct (le_dec d i); nf); f_equal;
[ rewrite IHs | rewrite IHs | rewrite IHu] ; eqs.
Qed.
Lemma subaboveexs : forall (t s : lam) (i j k : nat), j > i ->
exs k j (sub i t s) = sub i (exs k (S j) t) (exs k (j - i) s).
induction t; intros s i j k H; (destruct (le_dec n i); nf); f_equal;
[ destruct (Nat.eq_dec n i) | rewrite IHt | rewrite IHt1 | rewrite IHt2]; nf.
Qed.
Lemma subbelowexs : forall (t s : lam) (i j k : nat), j <= i ->
exs k j (sub i t s) = sub (i+k) (exs k j t) s.
induction t; intros s i j k H;(destruct (le_dec n i);nf); (destruct (le_dec j n);nf); f_equal;
[ destruct (Nat.eq_dec n i) | rewrite IHt | rewrite IHt1 | rewrite IHt2]; nf.
Qed.
Lemma subinexs : forall (k:nat)(u t: lam)(j d : nat), k < j ->
exs (j-1) d t = sub (k+d) (exs j d t) u.
intros k u t. induction t; intros j d H; (destruct (le_dec d n); nf); f_equal;
[ rewrite IHt | rewrite IHt1 | rewrite IHt2 ]; eqs.
Qed.
dcs (exs n d t) = exs n (d-1) (dcs t).
intros t d n Hd.
case t; intro i; case i; intros; simpl in * |-; try lia; elim (le_dec d (S n0)); intros; nf. Qed.
Lemma exsads : forall (t:lam)(i d k:nat), ~(d <= i) ->
exs k d (ads i t) = ads i (exs k (d-i) t).
intros t i d k Hd. elim (le_dec (d-i) (eos t)); case t; intros; nf. Qed.
Lemma dcsbul : forall (t:lam), eos t > 0 ->
dcs (bul t) = bul (dcs t).
intro t. case t; [ | | intros n u; case u]; intros; nf. Qed.
Lemma bulads : forall (t:lam)(n:nat),
bul (ads n t) = ads n (bul t).
intro t. case t; [ | | intros n u; case u]; intros; nf. Qed.
Hint Rewrite dcsexs exsads subgeads dcsbul using eqs : gldb.
Hint Rewrite <- bulads : gldb.
Lemma exsbelowexs : forall (t:lam)(e d k m:nat), d < e ->
exs m d (exs k e t) = exs k (e+m) (exs m d t).
intro t. elim t; [ intro i | intros i s IHs | intros i s IHs u IHu ]; intros e d k m H;
(destruct (le_dec d i); [ destruct (le_dec e i) |]; nf); f_equal;
[ rewrite IHs | rewrite IHs | rewrite IHu] ; eqs.
Qed.
Lemma exsinexs : forall (e:nat)(t:lam)(d k m:nat), e <= m ->
exs (k+m) d t = exs k (d+e) (exs m d t).
intros e t;elim t;[ intro i | intros i s IHs | intros i s IHs u IHu ]; intros d k m H;
(destruct (le_dec d i); nf); f_equal;
[ rewrite IHs | rewrite IHs | rewrite IHu] ; eqs.
Qed.
Lemma subaboveexs : forall (t s : lam) (i j k : nat), j > i ->
exs k j (sub i t s) = sub i (exs k (S j) t) (exs k (j - i) s).
induction t; intros s i j k H; (destruct (le_dec n i); nf); f_equal;
[ destruct (Nat.eq_dec n i) | rewrite IHt | rewrite IHt1 | rewrite IHt2]; nf.
Qed.
Lemma subbelowexs : forall (t s : lam) (i j k : nat), j <= i ->
exs k j (sub i t s) = sub (i+k) (exs k j t) s.
induction t; intros s i j k H;(destruct (le_dec n i);nf); (destruct (le_dec j n);nf); f_equal;
[ destruct (Nat.eq_dec n i) | rewrite IHt | rewrite IHt1 | rewrite IHt2]; nf.
Qed.
Lemma subinexs : forall (k:nat)(u t: lam)(j d : nat), k < j ->
exs (j-1) d t = sub (k+d) (exs j d t) u.
intros k u t. induction t; intros j d H; (destruct (le_dec d n); nf); f_equal;
[ rewrite IHt | rewrite IHt1 | rewrite IHt2 ]; eqs.
Qed.
TLFKASL; self-distributivity of substitution; cf. Schikora, MSc thesis, CL, Innsbruck, 2022.
The Lemma Formerly Known As Substitution Lemma (Barendregt, 1984)
Lemma subsub : forall (u t s: lam)(e d : nat), d <= e ->
sub d (sub (S e) t u) (sub (e - d) s u) =
sub e (sub d t s) u.
intros u t. induction t; intros s e d H; (destruct (le_dec n d); [ |
rewrite -> sublt with (s:=s); nf ; destruct (le_dec n (S e));
try (rewrite -> sublt with (d:=S e); [ | eqs])]; nf);
[ destruct (Nat.eq_dec n d); nf; rewrite subgeads
| destruct (Nat.eq_dec n (S e)) | f_equal; rewrite <- IHt
| f_equal; [rewrite <- IHt1 | rewrite <- IHt2]]; nf.
Qed.
Hint Rewrite <- subinexs using eqs : gldb.
Hint Rewrite exsbelowexs subbelowexs subaboveexs using eqs : gldb.
Hint Rewrite <- subsub using eqs : gldb.
Hint Rewrite <- exsinexs using eqs : gldb.
Lemma exsbul : forall (t : lam) (d n: nat),
exs n d (bul t) = bul (exs n d t).
induction t; intros d m; (destruct (le_dec d n); nf).
+ f_equal; rewrite IHt; nf.
+ revert IHt1. case t1; [intros i IHt1 | intros i t IHt1 | intros i t s IHt1]; nf;
try (rewrite IHt1; rewrite IHt2;nf);
(destruct (le_dec (d-n) i); nf; unfold beta; nf); rewrite <- IHt2; [
replace (S (d - n)) with (1+(d-n)); nf | ].
f_equal; f_equal; [ | eqs].
cut (exs m (d-n) (bul (abs i t)) = bul (exs m (d-n) (abs i t))).
nf. intro IHt1'. inversion IHt1'. symmetry. nf.
apply IHt1.
Qed.
Hint Rewrite exsbul : gldb.
sub d (sub (S e) t u) (sub (e - d) s u) =
sub e (sub d t s) u.
intros u t. induction t; intros s e d H; (destruct (le_dec n d); [ |
rewrite -> sublt with (s:=s); nf ; destruct (le_dec n (S e));
try (rewrite -> sublt with (d:=S e); [ | eqs])]; nf);
[ destruct (Nat.eq_dec n d); nf; rewrite subgeads
| destruct (Nat.eq_dec n (S e)) | f_equal; rewrite <- IHt
| f_equal; [rewrite <- IHt1 | rewrite <- IHt2]]; nf.
Qed.
Hint Rewrite <- subinexs using eqs : gldb.
Hint Rewrite exsbelowexs subbelowexs subaboveexs using eqs : gldb.
Hint Rewrite <- subsub using eqs : gldb.
Hint Rewrite <- exsinexs using eqs : gldb.
Lemma exsbul : forall (t : lam) (d n: nat),
exs n d (bul t) = bul (exs n d t).
induction t; intros d m; (destruct (le_dec d n); nf).
+ f_equal; rewrite IHt; nf.
+ revert IHt1. case t1; [intros i IHt1 | intros i t IHt1 | intros i t s IHt1]; nf;
try (rewrite IHt1; rewrite IHt2;nf);
(destruct (le_dec (d-n) i); nf; unfold beta; nf); rewrite <- IHt2; [
replace (S (d - n)) with (1+(d-n)); nf | ].
f_equal; f_equal; [ | eqs].
cut (exs m (d-n) (bul (abs i t)) = bul (exs m (d-n) (abs i t))).
nf. intro IHt1'. inversion IHt1'. symmetry. nf.
apply IHt1.
Qed.
Hint Rewrite exsbul : gldb.
beta steps of rewrite system, and (derived) reductions, as proof terms
Inductive step : lam -> lam -> Set :=
| sbeta (i j:nat) (t s:lam) : step (app i (abs j t) s) (ads i (beta j t s))
| sabs (i:nat) (t s:lam) : step t s -> step (abs i t) (abs i s)
| sapp1 (i:nat) (t s u:lam) : step t s -> step (app i t u) (app i s u)
| sapp2 (i:nat) (t s u:lam) : step t s -> step (app i u t) (app i u s).
| sbeta (i j:nat) (t s:lam) : step (app i (abs j t) s) (ads i (beta j t s))
| sabs (i:nat) (t s:lam) : step t s -> step (abs i t) (abs i s)
| sapp1 (i:nat) (t s u:lam) : step t s -> step (app i t u) (app i s u)
| sapp2 (i:nat) (t s u:lam) : step t s -> step (app i u t) (app i u s).
reductions as either non-empty compositions or empty,
so that empty steps do not proliferate
Inductive nred : lam -> lam -> Set :=
| nstep (t s:lam) : step t s -> nred t s
| ntrans (t s u:lam) : nred t s -> nred s u -> nred t u.
Inductive red : lam -> lam -> Set :=
| rrefl (t : lam) : red t t
| rnred (t s:lam) : nred t s -> red t s.
Create HintDb resgldb.
Hint Resolve sbeta sabs sapp1 sapp2 nstep rrefl rnred: resgldb.
Ltac rnf := nf; auto with resgldb.
| nstep (t s:lam) : step t s -> nred t s
| ntrans (t s u:lam) : nred t s -> nred s u -> nred t u.
Inductive red : lam -> lam -> Set :=
| rrefl (t : lam) : red t t
| rnred (t s:lam) : nred t s -> red t s.
Create HintDb resgldb.
Hint Resolve sbeta sabs sapp1 sapp2 nstep rrefl rnred: resgldb.
Ltac rnf := nf; auto with resgldb.
we have a term rewrite system: compatible, closed under substitutions, coherent
Definition rstep (t s:lam)(S:step t s): red t s := rnred (nstep S).
Definition rtrans t s u (R1 : red t s) : red s u -> red t u :=
match R1 in (red x1 y1) return (red y1 u -> red x1 u) with
| rrefl t1 => fun (R2 : red t1 u) => R2
| @rnred t1 s1 N1 => fun (R2 : red s1 u) =>
match R2 in (red x2 y2) return (nred t1 x2 -> red t1 y2) with
| rrefl t2 => rnred (s:=t2)
| @rnred t2 s2 N2 => (fun (n3 : nred t1 t2) => rnred (ntrans n3 N2))
end N1
end.
Lemma srr : forall (f: lam -> lam),
(forall (t s:lam), step t s -> red (f t) (f s)) ->
forall (t s:lam), red t s -> red (f t) (f s).
intros f H t s N. destruct N; rnf.
induction n; rnf.
apply rtrans with (s:=f s); [ exact IHn1 | exact IHn2 ].
Defined.
Lemma ssr : forall (f: lam -> lam),
(forall (t s:lam), step t s -> step (f t) (f s)) ->
forall (t s:lam), red t s -> red (f t) (f s).
intros f S; apply srr; intros t s T; rnf. Defined.
Lemma betatgt : forall (i j:nat)(t s u:lam),
ads i (beta j t s) = u -> step (app i (abs j t) s) u.
intros i j t s u H.
rewrite <- H; apply sbeta.
Defined.
Lemma ncrabsfw : forall (s t:lam), nred s t -> forall (i:nat)(u:lam), s = abs i u ->
{ v : lam & { r : nred u v | t = abs i v}}.
intros s t N. induction N; intros i x I;subst.
+ inversion s0; subst.
exists s1, (nstep H2); trivial.
+ cut {v : lam & {_ : nred x v | s = abs i v}}.
intro H1. destruct H1 as (w & I & J); subst.
cut {v : lam & {_ : nred w v | u = abs i v}}.
intro H1. destruct H1 as (y & K & L); subst.
exists y, (ntrans I K); trivial.
apply IHN2; trivial.
apply IHN1; trivial.
Defined.
Lemma sads : forall (i:nat) (t s:lam),
step t s -> step (ads i t) (ads i s).
intros i t s H. inversion H; rnf. Defined.
Lemma nrapp1 : forall (i :nat) (t s u:lam), nred t s -> nred (app i t u) (app i s u).
intros i t s u N. induction N; rnf. apply ntrans with (app i s u); trivial. Defined.
Lemma nrapp2 : forall (i :nat) (t s u:lam), nred t s -> nred (app i u t) (app i u s).
intros i t s u N. induction N; rnf. apply ntrans with (app i u s); trivial. Defined.
Hint Resolve sads nrapp1 nrapp2 : resgldb.
Lemma rabs : forall (i :nat) (t s:lam), red t s -> red (abs i t) (abs i s).
intros i t s R. destruct R as [|t s N]; [apply rrefl |apply rnred].
induction N; rnf. apply ntrans with (abs i s); trivial. Defined.
Lemma rads : forall (i:nat)(t s:lam), red t s ->
red (ads i t) (ads i s).
intro i; apply ssr with (f := fun u => ads i u); rnf. Defined.
Lemma rapp1 : forall (i :nat) (t s u:lam), red t s -> red (app i t u) (app i s u).
intros i t s u R. destruct R; rnf.
Defined.
Lemma rapp2 : forall (i :nat) (t s u:lam), red t s -> red (app i u t) (app i u s).
intros i t s u R. destruct R; rnf. Defined.
Hint Resolve rabs rapp1 rapp2 rads: resgldb.
Lemma crabsfw : forall (s t:lam), red s t -> forall (i:nat)(u:lam), s = abs i u ->
{ v : lam & { r : red u v | t = abs i v}}.
intros s t R. destruct R; intros i x N;subst.
+ exists x, (rrefl x). trivial.
+ cut { v : lam & { r : nred x v | s = abs i v}}.
intro H1. destruct H1 as (w & I & J); subst.
exists w, (rnred I); trivial.
apply ncrabsfw with (s:=abs i x); trivial.
Defined.
Lemma crabs : forall (i:nat)(u v:lam), red (abs i u) (abs i v) ->
red u v.
intros i u v R.
cut { v0 : lam & { r : red u v0 | abs i v = abs i v0}}.
intro H. destruct H as (x & I & J); subst.
inversion J; trivial.
apply crabsfw with (s:=abs i u)(t:=abs i v)(i:=i)(u:=u);trivial.
Defined.
Lemma rapp : forall (i :nat) (t s u v:lam), red t s -> red u v -> red (app i t u) (app i s v).
intros i t s u v R1 R2. apply rtrans with (app i s u); rnf. Defined.
Hint Resolve rapp crabs: resgldb.
Lemma sexs : forall (t s:lam), step t s -> forall (d k:nat),
step (exs k d t) (exs k d s).
intros t s S. induction S; intros d k; destruct (le_dec d i); rnf.
destruct (le_dec (d-i) j); nf; apply betatgt; f_equal; unfold beta; nf.
replace (S (d-i)) with (1+(d-i)); nf.
Defined.
Lemma sbsub : forall (t s:lam), step t s -> forall (i:nat)(u:lam),
step (sub i t u) (sub i s u).
intros t s S. induction S; intros k v; destruct (le_dec i k);rnf; destruct (le_dec j (k - i));rnf;
apply betatgt; unfold beta;rnf. f_equal; (f_equal;[| eqs]).
replace (S (k - i)) with ((k-i)+1);rnf.
Defined.
Lemma sasub : forall (t:lam)(i:nat)(u v:lam), step u v ->
red (sub i t u) (sub i t v).
induction t; intros i u v S; destruct (le_dec n i); rnf.
destruct (Nat.eq_dec n i); rnf.
Defined.
Hint Resolve sexs sasub sbsub: resgldb.
Lemma rexs : forall (d i:nat)(t s:lam), red t s ->
red (exs i d t) (exs i d s).
intros d i; apply ssr with (f:= fun u => exs i d u); rnf. Defined.
Lemma rbsub : forall (i:nat)(u t s:lam), red t s ->
red (sub i t u) (sub i s u).
intros i u; apply ssr with (f:= fun v => sub i v u); rnf. Defined.
Lemma rasub : forall (i:nat)(t u v:lam), red u v ->
red (sub i t u) (sub i t v).
intros i t; apply srr with (f:= fun s => sub i t s); rnf. Defined.
Hint Resolve rexs rasub rbsub: resgldb.
Lemma rsub : forall (t s u v:lam), red t s -> red u v -> forall (i:nat),
red (sub i t u) (sub i s v).
intros t s u v S R i; apply rtrans with (s:= sub i t v); rnf. Defined.
Hint Resolve rsub: resgldb.
Lemma rbeta : forall (t s u v:lam), red t s -> red u v -> forall (j:nat),
red (beta j t u) (beta j s v).
intros t s u v S R j. unfold beta. rnf. Defined.
Hint Resolve rbeta: resgldb.
Definition rtrans t s u (R1 : red t s) : red s u -> red t u :=
match R1 in (red x1 y1) return (red y1 u -> red x1 u) with
| rrefl t1 => fun (R2 : red t1 u) => R2
| @rnred t1 s1 N1 => fun (R2 : red s1 u) =>
match R2 in (red x2 y2) return (nred t1 x2 -> red t1 y2) with
| rrefl t2 => rnred (s:=t2)
| @rnred t2 s2 N2 => (fun (n3 : nred t1 t2) => rnred (ntrans n3 N2))
end N1
end.
Lemma srr : forall (f: lam -> lam),
(forall (t s:lam), step t s -> red (f t) (f s)) ->
forall (t s:lam), red t s -> red (f t) (f s).
intros f H t s N. destruct N; rnf.
induction n; rnf.
apply rtrans with (s:=f s); [ exact IHn1 | exact IHn2 ].
Defined.
Lemma ssr : forall (f: lam -> lam),
(forall (t s:lam), step t s -> step (f t) (f s)) ->
forall (t s:lam), red t s -> red (f t) (f s).
intros f S; apply srr; intros t s T; rnf. Defined.
Lemma betatgt : forall (i j:nat)(t s u:lam),
ads i (beta j t s) = u -> step (app i (abs j t) s) u.
intros i j t s u H.
rewrite <- H; apply sbeta.
Defined.
Lemma ncrabsfw : forall (s t:lam), nred s t -> forall (i:nat)(u:lam), s = abs i u ->
{ v : lam & { r : nred u v | t = abs i v}}.
intros s t N. induction N; intros i x I;subst.
+ inversion s0; subst.
exists s1, (nstep H2); trivial.
+ cut {v : lam & {_ : nred x v | s = abs i v}}.
intro H1. destruct H1 as (w & I & J); subst.
cut {v : lam & {_ : nred w v | u = abs i v}}.
intro H1. destruct H1 as (y & K & L); subst.
exists y, (ntrans I K); trivial.
apply IHN2; trivial.
apply IHN1; trivial.
Defined.
Lemma sads : forall (i:nat) (t s:lam),
step t s -> step (ads i t) (ads i s).
intros i t s H. inversion H; rnf. Defined.
Lemma nrapp1 : forall (i :nat) (t s u:lam), nred t s -> nred (app i t u) (app i s u).
intros i t s u N. induction N; rnf. apply ntrans with (app i s u); trivial. Defined.
Lemma nrapp2 : forall (i :nat) (t s u:lam), nred t s -> nred (app i u t) (app i u s).
intros i t s u N. induction N; rnf. apply ntrans with (app i u s); trivial. Defined.
Hint Resolve sads nrapp1 nrapp2 : resgldb.
Lemma rabs : forall (i :nat) (t s:lam), red t s -> red (abs i t) (abs i s).
intros i t s R. destruct R as [|t s N]; [apply rrefl |apply rnred].
induction N; rnf. apply ntrans with (abs i s); trivial. Defined.
Lemma rads : forall (i:nat)(t s:lam), red t s ->
red (ads i t) (ads i s).
intro i; apply ssr with (f := fun u => ads i u); rnf. Defined.
Lemma rapp1 : forall (i :nat) (t s u:lam), red t s -> red (app i t u) (app i s u).
intros i t s u R. destruct R; rnf.
Defined.
Lemma rapp2 : forall (i :nat) (t s u:lam), red t s -> red (app i u t) (app i u s).
intros i t s u R. destruct R; rnf. Defined.
Hint Resolve rabs rapp1 rapp2 rads: resgldb.
Lemma crabsfw : forall (s t:lam), red s t -> forall (i:nat)(u:lam), s = abs i u ->
{ v : lam & { r : red u v | t = abs i v}}.
intros s t R. destruct R; intros i x N;subst.
+ exists x, (rrefl x). trivial.
+ cut { v : lam & { r : nred x v | s = abs i v}}.
intro H1. destruct H1 as (w & I & J); subst.
exists w, (rnred I); trivial.
apply ncrabsfw with (s:=abs i x); trivial.
Defined.
Lemma crabs : forall (i:nat)(u v:lam), red (abs i u) (abs i v) ->
red u v.
intros i u v R.
cut { v0 : lam & { r : red u v0 | abs i v = abs i v0}}.
intro H. destruct H as (x & I & J); subst.
inversion J; trivial.
apply crabsfw with (s:=abs i u)(t:=abs i v)(i:=i)(u:=u);trivial.
Defined.
Lemma rapp : forall (i :nat) (t s u v:lam), red t s -> red u v -> red (app i t u) (app i s v).
intros i t s u v R1 R2. apply rtrans with (app i s u); rnf. Defined.
Hint Resolve rapp crabs: resgldb.
Lemma sexs : forall (t s:lam), step t s -> forall (d k:nat),
step (exs k d t) (exs k d s).
intros t s S. induction S; intros d k; destruct (le_dec d i); rnf.
destruct (le_dec (d-i) j); nf; apply betatgt; f_equal; unfold beta; nf.
replace (S (d-i)) with (1+(d-i)); nf.
Defined.
Lemma sbsub : forall (t s:lam), step t s -> forall (i:nat)(u:lam),
step (sub i t u) (sub i s u).
intros t s S. induction S; intros k v; destruct (le_dec i k);rnf; destruct (le_dec j (k - i));rnf;
apply betatgt; unfold beta;rnf. f_equal; (f_equal;[| eqs]).
replace (S (k - i)) with ((k-i)+1);rnf.
Defined.
Lemma sasub : forall (t:lam)(i:nat)(u v:lam), step u v ->
red (sub i t u) (sub i t v).
induction t; intros i u v S; destruct (le_dec n i); rnf.
destruct (Nat.eq_dec n i); rnf.
Defined.
Hint Resolve sexs sasub sbsub: resgldb.
Lemma rexs : forall (d i:nat)(t s:lam), red t s ->
red (exs i d t) (exs i d s).
intros d i; apply ssr with (f:= fun u => exs i d u); rnf. Defined.
Lemma rbsub : forall (i:nat)(u t s:lam), red t s ->
red (sub i t u) (sub i s u).
intros i u; apply ssr with (f:= fun v => sub i v u); rnf. Defined.
Lemma rasub : forall (i:nat)(t u v:lam), red u v ->
red (sub i t u) (sub i t v).
intros i t; apply srr with (f:= fun s => sub i t s); rnf. Defined.
Hint Resolve rexs rasub rbsub: resgldb.
Lemma rsub : forall (t s u v:lam), red t s -> red u v -> forall (i:nat),
red (sub i t u) (sub i s v).
intros t s u v S R i; apply rtrans with (s:= sub i t v); rnf. Defined.
Hint Resolve rsub: resgldb.
Lemma rbeta : forall (t s u v:lam), red t s -> red u v -> forall (j:nat),
red (beta j t u) (beta j s v).
intros t s u v S R j. unfold beta. rnf. Defined.
Hint Resolve rbeta: resgldb.
wrt the bullet map the rewrite system is extensive, has the rhs property,
and has Z (upperbound and monotonic)
Lemma extensive : forall t:lam, red t (bul t).
induction t; rnf.
revert IHt1; destruct t1 as [| m s |]; intros; rnf.
cut (red s (bul s)).
intro IHs. apply rtrans with (ads n (beta m s t2)); rnf.
apply crabs with (i:=m); trivial.
Defined.
induction t; rnf.
revert IHt1; destruct t1 as [| m s |]; intros; rnf.
cut (red s (bul s)).
intro IHs. apply rtrans with (ads n (beta m s t2)); rnf.
apply crabs with (i:=m); trivial.
Defined.
cf. the Nominal Isabelle formalisation of Z, Felgenhauer & Nagele & vO & Sternagel IWC 2016
Lemma appbul : forall (t s:lam)(i:nat),
red (app i (bul t) (bul s)) (bul (app i t s)).
intro t. destruct t; intros; rnf. Defined.
Hint Resolve extensive appbul: resgldb.
Lemma rhs : forall (t s:lam)(d:nat),
red (sub d (bul t) (bul s)) (bul (sub d t s)).
induction t; intros s d; destruct (le_dec n d) as [Hle | Hgt]; rnf;
[ destruct (Nat.eq_dec n d); rnf | ].
revert IHt1. case t1; [intros m IHt1 | intros m t IHt1 | intros m t u IHt1]; rnf.
+ apply rtrans with (app n (bul (sub (d-n) (var m) s)) (bul (sub (d-n) t2 s))); rnf.
+ destruct (le_dec m (d-n)) as [Ble | Bgt]; rnf.
- apply rads.
cut ((sub (d-n) (beta m (bul t) (bul t2)) (bul s)) =
(beta m (sub (S (d - n - m)) (bul t) (bul s))
(sub (d-n) (bul t2) (bul s)))).
* intro H. rewrite H.
apply rbeta; [|apply IHt2].
cut (red (sub (d-n) (bul (abs m t)) (bul s))
(bul (sub (d-n) (abs m t) s))).
nf.
intro IHt1dn. apply crabs in IHt1dn.
auto.
apply IHt1.
* unfold beta. rnf.
- replace (sub (d - n) (abs m t) s) with (dcs (abs m t)); nf.
apply rads.
cut ((sub (d - n) (beta m (bul t) (bul t2)) (bul s)) =
(beta (m - 1) (bul t) (sub (d-n) (bul t2) (bul s)))).
* intro H. rewrite H. rnf.
* unfold beta. nf. f_equal; [ |eqs]. rewrite <- exsbul.
replace (S (d-n)) with ((d-n)+1); [ |lia].
rewrite <- subinexs; rnf.
+ apply rtrans with (app n (bul (sub (d-n) (app m t u) s)) (bul (sub (d-n) t2 s))); rnf.
Defined.
Lemma upperbound : forall (t s:lam), step t s -> red s (bul t).
induction t; intros s S; [| | revert IHt1 S; case t1;
[ intros i IHt1 S | intros i t IHt1 S | intros i t u IHt1 S]]; inversion S; subst;rnf.
+ inversion H3;subst.
cut (red s (bul t)).
intros; apply rtrans with (ads n (beta i s t2)) ; rnf.
apply crabs with (i:=i). apply IHt1. trivial.
+ apply rtrans with (ads n (beta i t s0)) ; rnf.
Defined.
Hint Resolve rhs upperbound : resgldb.
Lemma monotonic : forall (t s:lam), step t s -> red (bul t) (bul s).
induction t; intros s S; [| | revert IHt1 S; case t1;
[ intros i IHt1 S | intros i t IHt1 S | intros i t u IHt1 S]]; inversion S; subst;rnf.
+ inversion H3.
+ rewrite bulads. apply rads. unfold beta. rnf.
+ inversion H3; subst. nf. apply rads.
cut (red (bul t) (bul s)).
intros. rnf.
apply crabs with (i:=i); apply IHt1 with (s:= abs i s); trivial.
+ apply rtrans with (s:= app n (bul s0) (bul t2)) ; rnf.
Defined.
Hint Resolve monotonic : resgldb.
red (app i (bul t) (bul s)) (bul (app i t s)).
intro t. destruct t; intros; rnf. Defined.
Hint Resolve extensive appbul: resgldb.
Lemma rhs : forall (t s:lam)(d:nat),
red (sub d (bul t) (bul s)) (bul (sub d t s)).
induction t; intros s d; destruct (le_dec n d) as [Hle | Hgt]; rnf;
[ destruct (Nat.eq_dec n d); rnf | ].
revert IHt1. case t1; [intros m IHt1 | intros m t IHt1 | intros m t u IHt1]; rnf.
+ apply rtrans with (app n (bul (sub (d-n) (var m) s)) (bul (sub (d-n) t2 s))); rnf.
+ destruct (le_dec m (d-n)) as [Ble | Bgt]; rnf.
- apply rads.
cut ((sub (d-n) (beta m (bul t) (bul t2)) (bul s)) =
(beta m (sub (S (d - n - m)) (bul t) (bul s))
(sub (d-n) (bul t2) (bul s)))).
* intro H. rewrite H.
apply rbeta; [|apply IHt2].
cut (red (sub (d-n) (bul (abs m t)) (bul s))
(bul (sub (d-n) (abs m t) s))).
nf.
intro IHt1dn. apply crabs in IHt1dn.
auto.
apply IHt1.
* unfold beta. rnf.
- replace (sub (d - n) (abs m t) s) with (dcs (abs m t)); nf.
apply rads.
cut ((sub (d - n) (beta m (bul t) (bul t2)) (bul s)) =
(beta (m - 1) (bul t) (sub (d-n) (bul t2) (bul s)))).
* intro H. rewrite H. rnf.
* unfold beta. nf. f_equal; [ |eqs]. rewrite <- exsbul.
replace (S (d-n)) with ((d-n)+1); [ |lia].
rewrite <- subinexs; rnf.
+ apply rtrans with (app n (bul (sub (d-n) (app m t u) s)) (bul (sub (d-n) t2 s))); rnf.
Defined.
Lemma upperbound : forall (t s:lam), step t s -> red s (bul t).
induction t; intros s S; [| | revert IHt1 S; case t1;
[ intros i IHt1 S | intros i t IHt1 S | intros i t u IHt1 S]]; inversion S; subst;rnf.
+ inversion H3;subst.
cut (red s (bul t)).
intros; apply rtrans with (ads n (beta i s t2)) ; rnf.
apply crabs with (i:=i). apply IHt1. trivial.
+ apply rtrans with (ads n (beta i t s0)) ; rnf.
Defined.
Hint Resolve rhs upperbound : resgldb.
Lemma monotonic : forall (t s:lam), step t s -> red (bul t) (bul s).
induction t; intros s S; [| | revert IHt1 S; case t1;
[ intros i IHt1 S | intros i t IHt1 S | intros i t u IHt1 S]]; inversion S; subst;rnf.
+ inversion H3.
+ rewrite bulads. apply rads. unfold beta. rnf.
+ inversion H3; subst. nf. apply rads.
cut (red (bul t) (bul s)).
intros. rnf.
apply crabs with (i:=i); apply IHt1 with (s:= abs i s); trivial.
+ apply rtrans with (s:= app n (bul s0) (bul t2)) ; rnf.
Defined.
Hint Resolve monotonic : resgldb.
(constructive) confluence from the Z-property via the Strip Lemma
Lemma rmonotonic : forall (t s:lam), red t s -> red (bul t) (bul s).
apply srr with (f:= bul). rnf. Defined.
Hint Resolve rmonotonic : resgldb.
Lemma stripZ : forall (t s u:lam), (step t s) -> (red t u) ->
{ v:lam & red s v & red u v }.
intros t s u R1 R2. exists (bul u); [ apply rtrans with (bul t) |]; rnf. Defined.
Theorem confluence : forall (t s:lam), (red t s) -> forall (u:lam), (red t u) ->
{ v:lam & red s v & red u v }.
intros t s R1.
destruct R1.
+ intros x R2. exists x; rnf.
+ induction n; intros x R2.
- apply stripZ with (t:=t); trivial.
- cut {w : lam & red s w & red x w}.
intro H. destruct H as [y].
cut {w : lam & red u w & red y w}.
intro H. destruct H as [z].
exists z; [ exact r1 | apply (rtrans r0 r2)].
apply IHn2; trivial.
apply IHn1; trivial.
Defined.
End ConfluencebyZ.
apply srr with (f:= bul). rnf. Defined.
Hint Resolve rmonotonic : resgldb.
Lemma stripZ : forall (t s u:lam), (step t s) -> (red t u) ->
{ v:lam & red s v & red u v }.
intros t s u R1 R2. exists (bul u); [ apply rtrans with (bul t) |]; rnf. Defined.
Theorem confluence : forall (t s:lam), (red t s) -> forall (u:lam), (red t u) ->
{ v:lam & red s v & red u v }.
intros t s R1.
destruct R1.
+ intros x R2. exists x; rnf.
+ induction n; intros x R2.
- apply stripZ with (t:=t); trivial.
- cut {w : lam & red s w & red x w}.
intro H. destruct H as [y].
cut {w : lam & red u w & red y w}.
intro H. destruct H as [z].
exists z; [ exact r1 | apply (rtrans r0 r2)].
apply IHn2; trivial.
apply IHn1; trivial.
Defined.
End ConfluencebyZ.
Some boiler-plate code to convert between dependently typed
proof terms for representing reductions as used above,
and non-dependently typed proof terms having a separate
well-formedness predicate, and source and target functions;
cf. Chapter 8 of Terese, Term Rewriting Systems, CUP, 2003.
Useful to avoid having to include source and target terms in reductions.
These then serve to demonstrate 2 simple examples of extraction
(result and result') of a valley witnessing confluence,
given a peak of reductions
Inductive inred : Set :=
| instep (t s:lam) : step t s -> inred
| intrans : inred -> inred -> inred.
Inductive ired : Set :=
| irrefl : lam -> ired
| irnred : inred -> ired.
Definition irtrans (R S:ired): ired :=
match R, S with
| irrefl _,_ => S
| irnred N1,irrefl _ => irnred N1
| irnred N1,irnred N2 => irnred (intrans N1 N2)
end.
Fixpoint insrc (N:inred) : lam := match N with
| @instep s _ _ => s
| intrans M _ => insrc M
end.
Fixpoint intgt (N:inred) : lam := match N with
| @instep _ t _ => t
| intrans _ M => intgt M
end.
Definition isrc (R:ired) : lam := match R with
| irrefl t => t
| irnred N => insrc N
end.
Definition itgt (R:ired) : lam := match R with
| irrefl t => t
| irnred N => intgt N
end.
Fixpoint inwf (N:inred) : Prop := match N with
| instep _ => True
| intrans N1 N2 => inwf N1 /\ intgt N1 = insrc N2 /\ inwf N2
end.
Definition iwf (R:ired) : Prop := match R with
| irrefl _ => True
| irnred N => inwf N
end.
Definition irtransok (r s:ired) := iwf r /\ itgt r = isrc s /\ iwf s.
Definition dep2wfok (s t:lam)(r:ired) := s = isrc r /\ iwf r /\ itgt r = t.
Lemma irtranswf : forall (r s: ired), irtransok r s -> dep2wfok (isrc r) (itgt s) (irtrans r s).
intros r s; case r,s; unfold irtransok;unfold dep2wfok; simpl;intros;intuition. Qed.
Lemma nwf2dep : forall (N:inred), inwf N -> nred (insrc N) (intgt N).
induction N; intro H; simpl.
+ apply nstep; exact s0.
+ destruct H as (wfsrc & srctgt & wftgt).
apply ntrans with (s:=intgt N1);
[ apply IHN1; exact wfsrc |
rewrite srctgt; apply IHN2; exact wftgt ].
Defined.
Lemma wf2dep : forall (R:ired), iwf R -> red (isrc R) (itgt R).
intro R.
destruct R; intro H; simpl in *.
+ apply rrefl.
+ apply rnred. apply nwf2dep. exact H.
Defined.
Lemma dep2wf : forall (s t:lam)(R:red s t), { r : ired | dep2wfok s t r}.
intros s t R.
destruct R.
+ exists (irrefl t); unfold dep2wfok; simpl; split; split; trivial.
+ induction n.
- exists (irnred (instep s0)); unfold dep2wfok; simpl; split; split; trivial.
- destruct IHn1.
destruct IHn2.
exists (irtrans x x0); subst.
unfold dep2wfok in *; simpl.
destruct d, d0. destruct H0, H2; subst.
cut (dep2wfok (isrc x) (itgt x0) (irtrans x x0)).
unfold dep2wfok.
intro H3.
destruct H3. destruct H3.
intuition.
apply irtranswf.
unfold irtransok.
intuition.
Defined.
Theorem confluencedep2wf (t s u:lam) : red t s -> red t u -> (ired * lam * ired)%type.
intros R S.
cut { v:lam & red s v & red u v }.
intro valley.
destruct valley.
cut { sx : ired | dep2wfok s x sx}.
cut { ux : ired | dep2wfok u x ux}.
intros Hux Hsx.
destruct Hux, Hsx.
exact (x0,x,x1).
apply dep2wf; trivial.
apply dep2wf; trivial.
apply confluence with (t:=t); trivial.
Defined.
Definition abs0 (t:lam) := abs 0 t.
Definition app0 (t s:lam) := app 0 t s.
Definition I := abs0 (var 0).
Definition mock := abs0 (app0 (var 0) (var 0)).
| instep (t s:lam) : step t s -> inred
| intrans : inred -> inred -> inred.
Inductive ired : Set :=
| irrefl : lam -> ired
| irnred : inred -> ired.
Definition irtrans (R S:ired): ired :=
match R, S with
| irrefl _,_ => S
| irnred N1,irrefl _ => irnred N1
| irnred N1,irnred N2 => irnred (intrans N1 N2)
end.
Fixpoint insrc (N:inred) : lam := match N with
| @instep s _ _ => s
| intrans M _ => insrc M
end.
Fixpoint intgt (N:inred) : lam := match N with
| @instep _ t _ => t
| intrans _ M => intgt M
end.
Definition isrc (R:ired) : lam := match R with
| irrefl t => t
| irnred N => insrc N
end.
Definition itgt (R:ired) : lam := match R with
| irrefl t => t
| irnred N => intgt N
end.
Fixpoint inwf (N:inred) : Prop := match N with
| instep _ => True
| intrans N1 N2 => inwf N1 /\ intgt N1 = insrc N2 /\ inwf N2
end.
Definition iwf (R:ired) : Prop := match R with
| irrefl _ => True
| irnred N => inwf N
end.
Definition irtransok (r s:ired) := iwf r /\ itgt r = isrc s /\ iwf s.
Definition dep2wfok (s t:lam)(r:ired) := s = isrc r /\ iwf r /\ itgt r = t.
Lemma irtranswf : forall (r s: ired), irtransok r s -> dep2wfok (isrc r) (itgt s) (irtrans r s).
intros r s; case r,s; unfold irtransok;unfold dep2wfok; simpl;intros;intuition. Qed.
Lemma nwf2dep : forall (N:inred), inwf N -> nred (insrc N) (intgt N).
induction N; intro H; simpl.
+ apply nstep; exact s0.
+ destruct H as (wfsrc & srctgt & wftgt).
apply ntrans with (s:=intgt N1);
[ apply IHN1; exact wfsrc |
rewrite srctgt; apply IHN2; exact wftgt ].
Defined.
Lemma wf2dep : forall (R:ired), iwf R -> red (isrc R) (itgt R).
intro R.
destruct R; intro H; simpl in *.
+ apply rrefl.
+ apply rnred. apply nwf2dep. exact H.
Defined.
Lemma dep2wf : forall (s t:lam)(R:red s t), { r : ired | dep2wfok s t r}.
intros s t R.
destruct R.
+ exists (irrefl t); unfold dep2wfok; simpl; split; split; trivial.
+ induction n.
- exists (irnred (instep s0)); unfold dep2wfok; simpl; split; split; trivial.
- destruct IHn1.
destruct IHn2.
exists (irtrans x x0); subst.
unfold dep2wfok in *; simpl.
destruct d, d0. destruct H0, H2; subst.
cut (dep2wfok (isrc x) (itgt x0) (irtrans x x0)).
unfold dep2wfok.
intro H3.
destruct H3. destruct H3.
intuition.
apply irtranswf.
unfold irtransok.
intuition.
Defined.
Theorem confluencedep2wf (t s u:lam) : red t s -> red t u -> (ired * lam * ired)%type.
intros R S.
cut { v:lam & red s v & red u v }.
intro valley.
destruct valley.
cut { sx : ired | dep2wfok s x sx}.
cut { ux : ired | dep2wfok u x ux}.
intros Hux Hsx.
destruct Hux, Hsx.
exact (x0,x,x1).
apply dep2wf; trivial.
apply dep2wf; trivial.
apply confluence with (t:=t); trivial.
Defined.
Definition abs0 (t:lam) := abs 0 t.
Definition app0 (t s:lam) := app 0 t s.
Definition I := abs0 (var 0).
Definition mock := abs0 (app0 (var 0) (var 0)).
the mockingbird; half of Omega
Definition Omega := app0 mock mock.
Definition Omegae := rrefl Omega.
Definition Omegal := rstep (sbeta 0 0 (app0 (var 0) (var 0)) mock).
Definition I5 := app0 I (var 5).
Definition II5 := app0 I I5.
Definition II5o := rstep (sapp2 2 I5 (sbeta 0 0 (var 0) I5)).
Definition II5i := rstep (sapp2 2 I5 (sapp2 0 I (sbeta 0 0 (var 0) (var 5)))).
Definition Omegae := rrefl Omega.
Definition Omegal := rstep (sbeta 0 0 (app0 (var 0) (var 0)) mock).
Definition I5 := app0 I (var 5).
Definition II5 := app0 I I5.
Definition II5o := rstep (sapp2 2 I5 (sbeta 0 0 (var 0) I5)).
Definition II5i := rstep (sapp2 2 I5 (sapp2 0 I (sbeta 0 0 (var 0) (var 5)))).
construct valleys for the following peaks
Definition result := confluencedep2wf II5o II5i.
Definition result' := confluencedep2wf Omegae Omegal.
Extraction Language Haskell.
Definition result' := confluencedep2wf Omegae Omegal.
Extraction Language Haskell.
extract to Haskell
Require Import ExtrHaskellBasic.
use functions from Haskell Prelude
Extraction "/Users/oostrom/Desktop/ConfluencebyZofGeneralisedLocalDeBruijninCoqExtracted" result result'.
Boiler-plate Haskell code to print result and result' in a separate file Boiler.hs