Library ConfluencebyZofGeneralisedLocalDeBruijninCoq
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).
- enable ssreflect tactics
From Coq Require Import ssreflect ssrfun ssrbool.
- to extract Haskell confluence function
From Coq Require Import Extraction.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
- scopes as unary natural numbers
Require Import Nat.
- automatic scope comparisons via lia
Require Import Psatz.
- move between bool and Prop for equality and comparison of scopes / nats
Require Import PeanoNat.
Require Import Compare_dec.
Require Import Compare_dec.
- using x_equation coming from Function x to avoid (some) boiler plate code
Require Import FunInd.
Section ConfluencebyZofGeneralisedLocalDeBruijninCoq.
Section ConfluencebyZofGeneralisedLocalDeBruijninCoq.
objects of rewrite system: generalised local De Bruijn terms, with operations for beta
and bullet function for Z
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.
| 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.
move=> n t. case t; intuition. Qed.
Lemma eosexs1 : forall (t:lam)(d e:nat), e <= eos t -> e <= eos (exs1 t d).
move=>t d; case t; simpl; move=> 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=>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).
move=>t; case t; [auto|auto|].
move=> n l; case l; [auto|move=>i u v j;simpl; rewrite eosads=>H;lia|auto]. Qed.
Ltac eqs :=
try (apply eosbul; first by eqs);
try (apply eosexs; first by eqs);
try (apply eosexs1; first by 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.
move=> n t. case t; intuition. Qed.
Lemma eosexs1 : forall (t:lam)(d e:nat), e <= eos t -> e <= eos (exs1 t d).
move=>t d; case t; simpl; move=> 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=>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).
move=>t; case t; [auto|auto|].
move=> n l; case l; [auto|move=>i u v j;simpl; rewrite eosads=>H;lia|auto]. Qed.
Ltac eqs :=
try (apply eosbul; first by eqs);
try (apply eosexs; first by eqs);
try (apply eosexs1; first by 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.
move=> n t. case t; simpl; move=> *; eqs. Qed.
Lemma dcsadst : forall (t:lam)(n:nat), eos t > 0 -> dcs (ads n t) = ads n (dcs t).
move=> t n. case t; simpl; move=> *; 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.
move=> t. case t; move=>* ; subst; eqs. Qed.
Lemma adsads : forall (n m:nat)(t:lam),
ads m (ads n t) = ads (n+m) t.
move=> n m t. case t;move=> *; 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.
move =>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 => d t H; rewrite exs_equation.
+ rewrite adszer; trivial.
+ rewrite IHn; [ apply eosexs1 |
rewrite exs1_equation; rewrite leb_correct; last rewrite adsads ]; trivial.
Qed.
Lemma exslevar : forall (n d:nat)(i:nat), d <= i -> exs n d (var i) = var (i+n).
move => *. 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.
move => *. 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.
move => *. 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.
move => *. rewrite exsle; first 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 => d t H; rewrite exs_equation.
+ case t; trivial.
+ rewrite exs1_equation. rewrite leb_correct_conv; first lia.
move: H. case t=>*; (rewrite IHn; simpl in *; [trivial | f_equal]).
Qed.
Lemma exsgtvar : forall (n d:nat)(i:nat), ~d <= i -> exs n d (var i) = var i.
move => *. 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).
move => *. 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).
move => *. rewrite exsgt; auto. Qed.
Lemma sublt : forall (t:lam)(d:nat)(s:lam), d < eos t ->
sub d t s = dcs t.
move=> t d s. case t;simpl;move=>*; (rewrite leb_correct_conv; [lia|trivial]). Qed.
Lemma subgtvar : forall (j d:nat)(s:lam), j < d ->
sub d (var j) s = (var j).
move=> j d s H; simpl; rewrite leb_correct; first lia.
have : (j =? d) = false by apply Nat.eqb_neq; first lia.
move=> R; rewrite R; trivial. Qed.
Lemma subeqvar : forall (j d:nat)(s:lam), j = d ->
sub d (var j) s = ads j s.
move =>*; simpl; rewrite leb_correct; [ lia | subst; rewrite Nat.eqb_refl; trivial]. 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).
move=>*; simpl; rewrite leb_correct; [lia | trivial]. 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).
move=>*. simpl. rewrite leb_correct; [ lia | trivial]. 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 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).
move=> t i k. destruct (le_dec (i+(eos t)) k) as [Hle | Hgt ];
[ move: Hle; case t=> n *; [ destruct (Nat.eq_dec (i+n) k) | |] | move =>*]; 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.
move=> n t. case t; simpl; move=> *; eqs. Qed.
Lemma dcsadst : forall (t:lam)(n:nat), eos t > 0 -> dcs (ads n t) = ads n (dcs t).
move=> t n. case t; simpl; move=> *; 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.
move=> t. case t; move=>* ; subst; eqs. Qed.
Lemma adsads : forall (n m:nat)(t:lam),
ads m (ads n t) = ads (n+m) t.
move=> n m t. case t;move=> *; 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.
move =>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 => d t H; rewrite exs_equation.
+ rewrite adszer; trivial.
+ rewrite IHn; [ apply eosexs1 |
rewrite exs1_equation; rewrite leb_correct; last rewrite adsads ]; trivial.
Qed.
Lemma exslevar : forall (n d:nat)(i:nat), d <= i -> exs n d (var i) = var (i+n).
move => *. 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.
move => *. 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.
move => *. 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.
move => *. rewrite exsle; first 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 => d t H; rewrite exs_equation.
+ case t; trivial.
+ rewrite exs1_equation. rewrite leb_correct_conv; first lia.
move: H. case t=>*; (rewrite IHn; simpl in *; [trivial | f_equal]).
Qed.
Lemma exsgtvar : forall (n d:nat)(i:nat), ~d <= i -> exs n d (var i) = var i.
move => *. 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).
move => *. 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).
move => *. rewrite exsgt; auto. Qed.
Lemma sublt : forall (t:lam)(d:nat)(s:lam), d < eos t ->
sub d t s = dcs t.
move=> t d s. case t;simpl;move=>*; (rewrite leb_correct_conv; [lia|trivial]). Qed.
Lemma subgtvar : forall (j d:nat)(s:lam), j < d ->
sub d (var j) s = (var j).
move=> j d s H; simpl; rewrite leb_correct; first lia.
have : (j =? d) = false by apply Nat.eqb_neq; first lia.
move=> R; rewrite R; trivial. Qed.
Lemma subeqvar : forall (j d:nat)(s:lam), j = d ->
sub d (var j) s = ads j s.
move =>*; simpl; rewrite leb_correct; [ lia | subst; rewrite Nat.eqb_refl; trivial]. 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).
move=>*; simpl; rewrite leb_correct; [lia | trivial]. 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).
move=>*. simpl. rewrite leb_correct; [ lia | trivial]. 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 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).
move=> t i k. destruct (le_dec (i+(eos t)) k) as [Hle | Hgt ];
[ move: Hle; case t=> n *; [ destruct (Nat.eq_dec (i+n) k) | |] | move =>*]; 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).
move=> t d n Hd.
case t=>i;(case i=>[*|j *]; simpl in * |-;[lia|]); (elim (le_dec d (S j)) => * ); 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).
move=> t i d k Hd. elim (le_dec (d-i) (eos t)); case t; move =>*; nf. Qed.
Lemma dcsbul : forall (t:lam), eos t > 0 ->
dcs (bul t) = bul (dcs t).
move=> t. case t; [ | | move => n u; case u]; move => *; nf. Qed.
Lemma bulads : forall (t:lam)(n:nat),
bul (ads n t) = ads n (bul t).
move=> t. case t; [ | | move => n u; case u]; move => *; 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).
move=> t. elim t => [ i | i s IHs | i s IHs u IHu ]; move=> 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).
move=> e t. elim t => [ i | i s IHs | i s IHs u IHu ]; move=> 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=> 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 => 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.
move => k u t. induction t => 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).
move=> t d n Hd.
case t=>i;(case i=>[*|j *]; simpl in * |-;[lia|]); (elim (le_dec d (S j)) => * ); 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).
move=> t i d k Hd. elim (le_dec (d-i) (eos t)); case t; move =>*; nf. Qed.
Lemma dcsbul : forall (t:lam), eos t > 0 ->
dcs (bul t) = bul (dcs t).
move=> t. case t; [ | | move => n u; case u]; move => *; nf. Qed.
Lemma bulads : forall (t:lam)(n:nat),
bul (ads n t) = ads n (bul t).
move=> t. case t; [ | | move => n u; case u]; move => *; 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).
move=> t. elim t => [ i | i s IHs | i s IHs u IHu ]; move=> 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).
move=> e t. elim t => [ i | i s IHs | i s IHs u IHu ]; move=> 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=> 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 => 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.
move => k u t. induction t => 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.
move => u t. induction t => 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); last 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 => d m; (destruct (le_dec d n); nf).
+ f_equal; rewrite IHt; nf.
+ move: IHt1. case t1 => [i IHt1 | i t IHt1 | 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; last eqs.
have : exs m (d-n) (bul (abs i t)) = bul (exs m (d-n) (abs i t)) by apply IHt1.
nf. move=>IHt1'. inversion IHt1'. symmetry. nf.
Qed.
Hint Rewrite exsbul : gldb.
Ltac rnf := nf; auto with gldb.
sub d (sub (S e) t u) (sub (e - d) s u) =
sub e (sub d t s) u.
move => u t. induction t => 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); last 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 => d m; (destruct (le_dec d n); nf).
+ f_equal; rewrite IHt; nf.
+ move: IHt1. case t1 => [i IHt1 | i t IHt1 | 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; last eqs.
have : exs m (d-n) (bul (abs i t)) = bul (exs m (d-n) (abs i t)) by apply IHt1.
nf. move=>IHt1'. inversion IHt1'. symmetry. nf.
Qed.
Hint Rewrite exsbul : gldb.
Ltac rnf := nf; auto with 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.
Hint Resolve sbeta sabs sapp1 sapp2 nstep rrefl rnred: gldb.
| 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.
Hint Resolve sbeta sabs sapp1 sapp2 nstep rrefl rnred: gldb.
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).
move=> 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).
move=> f S; apply srr; move=> 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.
move=> 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}}.
move=> s t N. induction N => i x I;subst.
+ inversion s0; subst.
exists s1, (nstep H2); trivial.
+ have : {v : lam & {_ : nred x v | s = abs i v}} by apply IHN1; trivial.
move=>H1. destruct H1 as (w & I & J); subst.
have : {v : lam & {_ : nred w v | u = abs i v}} by apply IHN2; trivial.
move=>H1. destruct H1 as (y & K & L); subst.
exists y, (ntrans I K); trivial.
Defined.
Lemma sads : forall (i:nat) (t s:lam),
step t s -> step (ads i t) (ads i s).
move=> 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).
move=> 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).
move=> i t s u N. induction N; rnf. apply ntrans with (app i u s); trivial. Defined.
Hint Resolve sads nrapp1 nrapp2 : gldb.
Lemma rabs : forall (i :nat) (t s:lam), red t s -> red (abs i t) (abs i s).
move=> 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).
move=> 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).
move=> 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).
move=> i t s u R. destruct R; rnf. Defined.
Hint Resolve rabs rapp1 rapp2 rads: gldb.
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}}.
move=> s t R. destruct R => i x N;subst.
+ exists x, (rrefl x). trivial.
+ have : { v : lam & { r : nred x v | s = abs i v}} by apply ncrabsfw with (s:=abs i x); trivial.
move=>H1. destruct H1 as (w & I & J); subst.
exists w, (rnred I); trivial.
Defined.
Lemma crabs : forall (i:nat)(u v:lam), red (abs i u) (abs i v) ->
red u v.
move=> i u v R.
have : { v0 : lam & { r : red u v0 | abs i v = abs i v0}} by
apply crabsfw with (s:=abs i u)(t:=abs i v)(i:=i)(u:=u).
move=>H. destruct H as (x & I & J); subst.
inversion J; 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).
move=> i t s u v R1 R2. apply rtrans with (app i s u); rnf. Defined.
Hint Resolve rapp crabs: gldb.
Lemma sexs : forall (t s:lam), step t s -> forall (d k:nat),
step (exs k d t) (exs k d s).
move=> t s S. induction S => 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).
move=> t s S. induction S => k v; destruct (le_dec i k);rnf; destruct (le_dec j (k - i));rnf;
apply betatgt; unfold beta;rnf. f_equal; (f_equal;last 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=> i u v S; destruct (le_dec n i); rnf.
destruct (Nat.eq_dec n i); rnf.
Defined.
Hint Resolve sexs sasub sbsub: gldb.
Lemma rexs : forall (d i:nat)(t s:lam), red t s ->
red (exs i d t) (exs i d s).
move=> 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).
move=> 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).
move=> i t; apply srr with (f:= fun s => sub i t s); rnf. Defined.
Hint Resolve rexs rasub rbsub: gldb.
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).
move=> t s u v S R i; apply rtrans with (s:= sub i t v); rnf. Defined.
Hint Resolve rsub: gldb.
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).
move=> t s u v S R j. unfold beta. rnf. Defined.
Hint Resolve rbeta: gldb.
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).
move=> 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).
move=> f S; apply srr; move=> 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.
move=> 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}}.
move=> s t N. induction N => i x I;subst.
+ inversion s0; subst.
exists s1, (nstep H2); trivial.
+ have : {v : lam & {_ : nred x v | s = abs i v}} by apply IHN1; trivial.
move=>H1. destruct H1 as (w & I & J); subst.
have : {v : lam & {_ : nred w v | u = abs i v}} by apply IHN2; trivial.
move=>H1. destruct H1 as (y & K & L); subst.
exists y, (ntrans I K); trivial.
Defined.
Lemma sads : forall (i:nat) (t s:lam),
step t s -> step (ads i t) (ads i s).
move=> 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).
move=> 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).
move=> i t s u N. induction N; rnf. apply ntrans with (app i u s); trivial. Defined.
Hint Resolve sads nrapp1 nrapp2 : gldb.
Lemma rabs : forall (i :nat) (t s:lam), red t s -> red (abs i t) (abs i s).
move=> 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).
move=> 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).
move=> 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).
move=> i t s u R. destruct R; rnf. Defined.
Hint Resolve rabs rapp1 rapp2 rads: gldb.
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}}.
move=> s t R. destruct R => i x N;subst.
+ exists x, (rrefl x). trivial.
+ have : { v : lam & { r : nred x v | s = abs i v}} by apply ncrabsfw with (s:=abs i x); trivial.
move=>H1. destruct H1 as (w & I & J); subst.
exists w, (rnred I); trivial.
Defined.
Lemma crabs : forall (i:nat)(u v:lam), red (abs i u) (abs i v) ->
red u v.
move=> i u v R.
have : { v0 : lam & { r : red u v0 | abs i v = abs i v0}} by
apply crabsfw with (s:=abs i u)(t:=abs i v)(i:=i)(u:=u).
move=>H. destruct H as (x & I & J); subst.
inversion J; 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).
move=> i t s u v R1 R2. apply rtrans with (app i s u); rnf. Defined.
Hint Resolve rapp crabs: gldb.
Lemma sexs : forall (t s:lam), step t s -> forall (d k:nat),
step (exs k d t) (exs k d s).
move=> t s S. induction S => 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).
move=> t s S. induction S => k v; destruct (le_dec i k);rnf; destruct (le_dec j (k - i));rnf;
apply betatgt; unfold beta;rnf. f_equal; (f_equal;last 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=> i u v S; destruct (le_dec n i); rnf.
destruct (Nat.eq_dec n i); rnf.
Defined.
Hint Resolve sexs sasub sbsub: gldb.
Lemma rexs : forall (d i:nat)(t s:lam), red t s ->
red (exs i d t) (exs i d s).
move=> 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).
move=> 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).
move=> i t; apply srr with (f:= fun s => sub i t s); rnf. Defined.
Hint Resolve rexs rasub rbsub: gldb.
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).
move=> t s u v S R i; apply rtrans with (s:= sub i t v); rnf. Defined.
Hint Resolve rsub: gldb.
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).
move=> t s u v S R j. unfold beta. rnf. Defined.
Hint Resolve rbeta: gldb.
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.
move: IHt1; destruct t1 as [| m s |]; move =>*; rnf.
have : red s (bul s) by apply crabs with (i:=m). move => IHs.
apply rtrans with (ads n (beta m s t2)); rnf.
Defined.
induction t; rnf.
move: IHt1; destruct t1 as [| m s |]; move =>*; rnf.
have : red s (bul s) by apply crabs with (i:=m). move => IHs.
apply rtrans with (ads n (beta m s t2)); rnf.
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)).
move=>t. destruct t; move=>*; rnf. Defined.
Hint Resolve extensive appbul: gldb.
Lemma rhs : forall (t s:lam)(d:nat),
red (sub d (bul t) (bul s)) (bul (sub d t s)).
induction t => s d; destruct (le_dec n d) as [Hle | Hgt]; rnf;
[ destruct (Nat.eq_dec n d); rnf | ].
move: IHt1. case t1 => [ m IHt1 | m t IHt1 | 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.
have : (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))).
* unfold beta. rnf.
* move=> H. rewrite H.
apply rbeta; [|apply IHt2].
have : red (sub (d-n) (bul (abs m t)) (bul s))
(bul (sub (d-n) (abs m t) s)) by apply IHt1.
nf.
move=> IHt1dn. apply crabs in IHt1dn.
auto.
- rewrite [sub _ (abs _ _ ) _]sublt; nf.
apply rads.
have : (sub (d - n) (beta m (bul t) (bul t2)) (bul s)) =
(beta (m - 1) (bul t) (sub (d-n) (bul t2) (bul s))).
* unfold beta. nf. f_equal; last eqs. rewrite <- exsbul.
replace (S (d-n)) with ((d-n)+1); last lia.
rewrite <- subinexs; rnf.
* move=> H. rewrite H. 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 => s S; [| | move: IHt1 S; case t1 =>
[ i IHt1 S | i t IHt1 S | i t u IHt1 S]]; inversion S; subst;rnf.
+ inversion H3;subst.
have : red s (bul t) by apply crabs with (i:=i); apply IHt1. move => *.
apply rtrans with (ads n (beta i s t2)) ; rnf.
+ apply rtrans with (ads n (beta i t s0)) ; rnf.
Defined.
Hint Resolve rhs upperbound : gldb.
Lemma monotonic : forall (t s:lam), step t s -> red (bul t) (bul s).
induction t => s S; [| | move: IHt1 S; case t1 =>
[ i IHt1 S | i t IHt1 S | i t u IHt1 S]]; inversion S; subst;rnf.
+ inversion H3.
+ rewrite bulads. apply rads. unfold beta. rnf.
+ inversion H3; subst. nf. apply rads.
have : red (bul t) (bul s) by apply crabs with (i:=i); apply IHt1 with (s:= abs i s). move => *.
rnf.
+ apply rtrans with (s:= app n (bul s0) (bul t2)) ; rnf.
Defined.
Hint Resolve monotonic : gldb.
red (app i (bul t) (bul s)) (bul (app i t s)).
move=>t. destruct t; move=>*; rnf. Defined.
Hint Resolve extensive appbul: gldb.
Lemma rhs : forall (t s:lam)(d:nat),
red (sub d (bul t) (bul s)) (bul (sub d t s)).
induction t => s d; destruct (le_dec n d) as [Hle | Hgt]; rnf;
[ destruct (Nat.eq_dec n d); rnf | ].
move: IHt1. case t1 => [ m IHt1 | m t IHt1 | 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.
have : (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))).
* unfold beta. rnf.
* move=> H. rewrite H.
apply rbeta; [|apply IHt2].
have : red (sub (d-n) (bul (abs m t)) (bul s))
(bul (sub (d-n) (abs m t) s)) by apply IHt1.
nf.
move=> IHt1dn. apply crabs in IHt1dn.
auto.
- rewrite [sub _ (abs _ _ ) _]sublt; nf.
apply rads.
have : (sub (d - n) (beta m (bul t) (bul t2)) (bul s)) =
(beta (m - 1) (bul t) (sub (d-n) (bul t2) (bul s))).
* unfold beta. nf. f_equal; last eqs. rewrite <- exsbul.
replace (S (d-n)) with ((d-n)+1); last lia.
rewrite <- subinexs; rnf.
* move=> H. rewrite H. 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 => s S; [| | move: IHt1 S; case t1 =>
[ i IHt1 S | i t IHt1 S | i t u IHt1 S]]; inversion S; subst;rnf.
+ inversion H3;subst.
have : red s (bul t) by apply crabs with (i:=i); apply IHt1. move => *.
apply rtrans with (ads n (beta i s t2)) ; rnf.
+ apply rtrans with (ads n (beta i t s0)) ; rnf.
Defined.
Hint Resolve rhs upperbound : gldb.
Lemma monotonic : forall (t s:lam), step t s -> red (bul t) (bul s).
induction t => s S; [| | move: IHt1 S; case t1 =>
[ i IHt1 S | i t IHt1 S | i t u IHt1 S]]; inversion S; subst;rnf.
+ inversion H3.
+ rewrite bulads. apply rads. unfold beta. rnf.
+ inversion H3; subst. nf. apply rads.
have : red (bul t) (bul s) by apply crabs with (i:=i); apply IHt1 with (s:= abs i s). move => *.
rnf.
+ apply rtrans with (s:= app n (bul s0) (bul t2)) ; rnf.
Defined.
Hint Resolve monotonic : gldb.
(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 : gldb.
Lemma stripZ : forall (t s u:lam), (step t s) -> (red t u) ->
{ v:lam & red s v & red u v }.
move=> 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 }.
move=>t s R1.
destruct R1.
+ move=> x R2. exists x; rnf.
+ induction n => x R2.
- apply stripZ with (t:=t); trivial.
- have : {w : lam & red s w & red x w} by apply IHn1; trivial.
move=> H. destruct H as [y].
have : {w : lam & red u w & red y w} by apply IHn2; trivial.
move=> H. destruct H as [z].
exists z; [ exact r1 | apply (rtrans r0 r2)].
Defined.
End ConfluencebyZofGeneralisedLocalDeBruijninCoq.
Extraction Language Haskell.
Extraction "/Users/oostromgestolen/Desktop/ConfluencebyZofGeneralisedLocalDeBruijninCoqExtracted" confluence.
apply srr with (f:= bul). rnf. Defined.
Hint Resolve rmonotonic : gldb.
Lemma stripZ : forall (t s u:lam), (step t s) -> (red t u) ->
{ v:lam & red s v & red u v }.
move=> 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 }.
move=>t s R1.
destruct R1.
+ move=> x R2. exists x; rnf.
+ induction n => x R2.
- apply stripZ with (t:=t); trivial.
- have : {w : lam & red s w & red x w} by apply IHn1; trivial.
move=> H. destruct H as [y].
have : {w : lam & red u w & red y w} by apply IHn2; trivial.
move=> H. destruct H as [z].
exists z; [ exact r1 | apply (rtrans r0 r2)].
Defined.
End ConfluencebyZofGeneralisedLocalDeBruijninCoq.
Extraction Language Haskell.
Extraction "/Users/oostromgestolen/Desktop/ConfluencebyZofGeneralisedLocalDeBruijninCoqExtracted" confluence.
Haskell extraction needs boiler plate code to interact with the confluence function; DIY