(** 
Changelog June 2026:
- 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
*)

(**
Confluence by Z of Generalised Local De Bruijn in Coq.
Vincent van Oostrom. oostrom@javakade.nl. www.javakade.nl 

Constructive confluence is derived from the Z-property (vO, FSCD 2021) 
for the rewrite system having as objects generalised De Bruijn terms 
(Bird & Paterson, JFP 1999) in a local representation (simplified from 
David & Guillaume, MSCS 2001), and as steps beta, decomposed into 
minimal scope extrusion and substitution, <<exs>> and <<sub>> 
(vO & van der Looij & Zwitserlood, ALPS 2004).

Developed with CoqIDE in Coq 8.16.1 on Mac OS X. December 2022.
Minimally commented version. Comments welcome.

For the ideas on which this formalisation is based, see De Bruijn, KNAW 1972, 
Berkling, GMD 1976, Huet JFP 1994, the works mentioned above, (Hendriks & vO, CADE 2003), and 
(vO & de Vrijer, Chapter 8 of Terese 2003). 
The lemmata governing the interaction between minimal scope 
extrusion and substitution are novel, afaik,
though they were already established in (Huet JFP 1994) for, 
what we would call, maximal scope extrusion and substitution, 
called <<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).

This work is licensed under the Creative Commons Attribution 4.0 
International License. To view a copy of this license, visit
http://creativecommons.org/licenses/by/4.0/. *)

(** - to extract Haskell confluence function *)
(** - From Stdlib Require Import Extraction. *)
From Corelib Require Extraction.
(** - enable ssreflect tactics *)
(** From Stdlib Require Import ssreflect ssrfun ssrbool.*)
Set Implicit Arguments.
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.
(** - 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.
(** 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.
(** 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.
(** 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.
(** 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.
(** 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.
(** 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.
(**  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).
(** 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.
(** 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.
(** 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.
(** 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.
(** (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. 

(** 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.

(* the simple lambda-terms for show-casing constructiveness of the confluence proof *)
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)))).

(** construct valleys for the following peaks *)
Definition result := confluencedep2wf II5o II5i.
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 *)