Built with Alectryon, running Coq+SerAPI v8.16.0+0.16.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
From Coq Require Import
  Relations.Relations
  Classes.RelationClasses.
From Tealeaves Require Import
  Backends.DB.

Import DecoratedTraversableMonad.UsefulInstances.

#[local] Set Implicit Arguments.

Import DB.Notations.

Inductive lam (V: Type) :=
| tvar: V -> lam V
| abs: lam V -> lam V
| app: lam V -> lam V -> lam V.

Fixpoint binddt_lam (G: Type -> Type) `{Map G} `{Pure G} `{Mult G}
    {v1 v2: Type} (f: nat * v1 -> G (lam v2)) (t: lam v1): G (lam v2) :=
  match t with
  | tvar v    => f (0, v)
  | abs body  => pure (@abs v2) <⋆> binddt_lam (f ⦿ 1) body
  | app t1 t2 => pure (@app v2) <⋆> binddt_lam f t1 <⋆> binddt_lam f t2
  end.

#[export] Instance Return_Lam: Return lam := tvar.
#[export] Instance Binddt_Lam: Binddt nat lam lam := @binddt_lam.

DecoratedTraversableMonad nat lam


DecoratedTraversableMonad nat lam

  derive_dtm.
Qed.


DecoratedTraversableMonad nat lam


DecoratedTraversableMonad nat lam

  
Monoid nat
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : nat * A -> G (lam B)),
binddt f ∘ ret = f ∘ ret
DecoratedTraversableRightPreModule nat lam lam

  
Monoid nat
 typeclasses eauto.
  
forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (A B : Type) (f : nat * A -> G (lam B)),
binddt f ∘ ret = f ∘ ret
 
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: nat * A -> G (lam B)
binddt f ∘ ret = f ∘ ret

    reflexivity.
  
DecoratedTraversableRightPreModule nat lam lam
 
forall A : Type, binddt (ret ∘ extract) = id
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall (B C : Type) (g : nat * B -> G2 (lam C))
  (A : Type) (f : nat * A -> G1 (lam B)),
map (binddt g) ∘ binddt f = binddt (g ⋆7 f)
forall (G1 G2 : Type -> Type) (H : Map G1)
  (H0 : Mult G1) (H1 : Pure G1) (H2 : Map G2)
  (H3 : Mult G2) (H4 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : nat * A -> G1 (lam B)),
ϕ (lam B) ∘ binddt f = binddt (ϕ (lam B) ∘ f)

    
forall A : Type, binddt (ret ∘ extract) = id
 
A: Type
binddt (ret ∘ extract) = id
 
A: Type
t: lam A
binddt (ret ∘ extract) t = id t

      
A: Type
v: A
binddt (ret ∘ extract) (tvar v) = id (tvar v)
A: Type
t: lam A
IHt: binddt (ret ∘ extract) t = id t
binddt (ret ∘ extract) (abs t) = id (abs t)
A: Type
t1, t2: lam A
IHt1: binddt (ret ∘ extract) t1 = id t1
IHt2: binddt (ret ∘ extract) t2 = id t2
binddt (ret ∘ extract) (app t1 t2) = id (app t1 t2)

      
A: Type
v: A
binddt (ret ∘ extract) (tvar v) = id (tvar v)
 reflexivity.
      
A: Type
t: lam A
IHt: binddt (ret ∘ extract) t = id t
binddt (ret ∘ extract) (abs t) = id (abs t)
 
A: Type
t: lam A
IHt: binddt (ret ∘ extract) t = id t
pure (abs (V:=A)) (binddt ((ret ∘ extract) ⦿ 1) t) =
id (abs t)

        
A: Type
t: lam A
IHt: binddt (ret ∘ extract) t = id t
pure (abs (V:=A)) (binddt ((ret ∘ extract) ⦿ 1) t) =
abs t

        
A: Type
t: lam A
IHt: binddt (ret ∘ extract) t = id t
abs (binddt ((ret ∘ extract) ⦿ 1) t) = abs t

        
A: Type
t: lam A
IHt: binddt (ret ∘ extract) t = id t
abs (binddt (ret ∘ extract) t) = abs t

        
A: Type
t: lam A
IHt: binddt (ret ∘ extract) t = id t
abs (id t) = abs t

        reflexivity.
      
A: Type
t1, t2: lam A
IHt1: binddt (ret ∘ extract) t1 = id t1
IHt2: binddt (ret ∘ extract) t2 = id t2
binddt (ret ∘ extract) (app t1 t2) = id (app t1 t2)
 
A: Type
t1, t2: lam A
IHt1: binddt (ret ∘ extract) t1 = id t1
IHt2: binddt (ret ∘ extract) t2 = id t2
pure (app (V:=A)) (binddt (ret ∘ extract) t1)
  (binddt (ret ∘ extract) t2) = id (app t1 t2)

        
A: Type
t1, t2: lam A
IHt1: binddt (ret ∘ extract) t1 = id t1
IHt2: binddt (ret ∘ extract) t2 = id t2
pure (app (V:=A)) (binddt (ret ∘ extract) t1)
  (binddt (ret ∘ extract) t2) = app t1 t2

        
A: Type
t1, t2: lam A
IHt1: binddt (ret ∘ extract) t1 = id t1
IHt2: binddt (ret ∘ extract) t2 = id t2
app (binddt (ret ∘ extract) t1)
  (binddt (ret ∘ extract) t2) = app t1 t2

        
A: Type
t1, t2: lam A
IHt1: binddt (ret ∘ extract) t1 = id t1
IHt2: binddt (ret ∘ extract) t2 = id t2
app (id t1) (binddt (ret ∘ extract) t2) = app t1 t2

        
A: Type
t1, t2: lam A
IHt1: binddt (ret ∘ extract) t1 = id t1
IHt2: binddt (ret ∘ extract) t2 = id t2
app (id t1) (id t2) = app t1 t2

        reflexivity.
    
forall (G1 : Type -> Type) (Map_G : Map G1)
  (Pure_G : Pure G1) (Mult_G : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G0 : Map G2)
  (Pure_G0 : Pure G2) (Mult_G0 : Mult G2),
Applicative G2 ->
forall (B C : Type) (g : nat * B -> G2 (lam C))
  (A : Type) (f : nat * A -> G1 (lam B)),
map (binddt g) ∘ binddt f = binddt (g ⋆7 f)
 
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C: Type
g: nat * B -> G2 (lam C)
A: Type
f: nat * A -> G1 (lam B)
map (binddt g) ∘ binddt f = binddt (g ⋆7 f)
 
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C: Type
g: nat * B -> G2 (lam C)
A: Type
f: nat * A -> G1 (lam B)
t: lam A
(map (binddt g) ∘ binddt f) t = binddt (g ⋆7 f) t

      
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C: Type
g: nat * B -> G2 (lam C)
A: Type
f: nat * A -> G1 (lam B)
t: lam A
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t

      
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C: Type
g: nat * B -> G2 (lam C)
A: Type
t: lam A
forall f : nat * A -> G1 (lam B),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t

      
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t

      
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
v: A
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (binddt g) (binddt f (tvar v)) =
binddt (g ⋆7 f) (tvar v)
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
IHt: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (binddt g) (binddt f (abs t)) =
binddt (g ⋆7 f) (abs t)
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (binddt g) (binddt f (app t1 t2)) =
binddt (g ⋆7 f) (app t1 t2)

      
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
v: A
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (binddt g) (binddt f (tvar v)) =
binddt (g ⋆7 f) (tvar v)
 
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
v: A
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (binddt g) (f (0, v)) =
map (binddt (g ⦿ 0)) (f (0, v))

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
v: A
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (binddt g) (f (Ƶ : nat, v)) =
map (binddt (g ⦿ (Ƶ : nat))) (f (Ƶ : nat, v))

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
v: A
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (binddt g) (f (Ƶ, v)) = map (binddt g) (f (Ƶ, v))

        reflexivity.
      
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
IHt: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (binddt g) (binddt f (abs t)) =
binddt (g ⋆7 f) (abs t)
 
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
IHt: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (binddt g)
  (pure (abs (V:=B)) <⋆> binddt (f ⦿ 1) t) =
pure (abs (V:=C)) <⋆> binddt ((g ⋆7 f) ⦿ 1) t

        (* LHS *)
        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
IHt: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (compose (binddt g)) (pure (abs (V:=B))) <⋆>
binddt (f ⦿ 1) t =
pure (abs (V:=C)) <⋆> binddt ((g ⋆7 f) ⦿ 1) t

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
IHt: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (binddt g ∘ abs (V:=B)) <⋆> binddt (f ⦿ 1) t =
pure (abs (V:=C)) <⋆> binddt ((g ⋆7 f) ⦿ 1) t

        (* RHS *)
        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
IHt: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (binddt g ∘ abs (V:=B)) <⋆> binddt (f ⦿ 1) t =
pure (pure (abs (V:=C))) <⋆> binddt ((g ⋆7 f) ⦿ 1) t

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
IHt: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (binddt g ∘ abs (V:=B)) <⋆> binddt (f ⦿ 1) t =
map (ap G2) (pure (pure (abs (V:=C)))) <⋆>
binddt ((g ⋆7 f) ⦿ 1) t

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
IHt: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (binddt g ∘ abs (V:=B)) <⋆> binddt (f ⦿ 1) t =
pure (ap G2 (pure (abs (V:=C)))) <⋆>
binddt ((g ⋆7 f) ⦿ 1) t

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
IHt: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (binddt g ∘ abs (V:=B)) <⋆> binddt (f ⦿ 1) t =
pure (ap G2 (pure (abs (V:=C)))) <⋆>
binddt (g ⦿ 1 ⋆7 f ⦿ 1) t

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
IHt: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (binddt g ∘ abs (V:=B)) <⋆> binddt (f ⦿ 1) t =
pure (ap G2 (pure (abs (V:=C)))) <⋆>
map (binddt (g ⦿ 1)) (binddt (f ⦿ 1) t)

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
IHt: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (binddt g ∘ abs (V:=B)) <⋆> binddt (f ⦿ 1) t =
map (precompose (binddt (g ⦿ 1)))
  (pure (ap G2 (pure (abs (V:=C))))) <⋆>
binddt (f ⦿ 1) t

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t: lam A
IHt: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t) = binddt (g ⋆7 f) t
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (binddt g ∘ abs (V:=B)) <⋆> binddt (f ⦿ 1) t =
pure
  (precompose (binddt (g ⦿ 1))
     (ap G2 (pure (abs (V:=C))))) <⋆> binddt (f ⦿ 1) t

        reflexivity.
      
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (binddt g) (binddt f (app t1 t2)) =
binddt (g ⋆7 f) (app t1 t2)
 
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (binddt g)
  (pure (app (V:=B)) <⋆> binddt f t1 <⋆> binddt f t2) =
pure (app (V:=C)) <⋆> binddt (g ⋆7 f) t1 <⋆>
binddt (g ⋆7 f) t2

        (* LHS *)
        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (compose (binddt g))
  (pure (app (V:=B)) <⋆> binddt f t1) <⋆> binddt f t2 =
pure (app (V:=C)) <⋆> binddt (g ⋆7 f) t1 <⋆>
binddt (g ⋆7 f) t2

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
map (compose (compose (binddt g))) (pure (app (V:=B))) <⋆>
binddt f t1 <⋆> binddt f t2 =
pure (app (V:=C)) <⋆> binddt (g ⋆7 f) t1 <⋆>
binddt (g ⋆7 f) t2

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
pure (app (V:=C)) <⋆> binddt (g ⋆7 f) t1 <⋆>
binddt (g ⋆7 f) t2

        (* RHS *)
        (* IHt1 *)
        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
pure (app (V:=C)) <⋆> map (binddt g) (binddt f t1) <⋆>
binddt (g ⋆7 f) t2

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
pure (pure (app (V:=C))) <⋆>
map (binddt g) (binddt f t1) <⋆> binddt (g ⋆7 f) t2

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
map (ap G2) (pure (pure (app (V:=C)))) <⋆>
map (binddt g) (binddt f t1) <⋆> binddt (g ⋆7 f) t2

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
pure (ap G2 (pure (app (V:=C)))) <⋆>
map (binddt g) (binddt f t1) <⋆> binddt (g ⋆7 f) t2

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
map (precompose (binddt g))
  (pure (ap G2 (pure (app (V:=C))))) <⋆> binddt f t1 <⋆>
binddt (g ⋆7 f) t2

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
pure
  (precompose (binddt g) (ap G2 (pure (app (V:=C))))) <⋆>
binddt f t1 <⋆> binddt (g ⋆7 f) t2

        (* IHt2 *)
        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
map (ap G2)
  (pure
     (precompose (binddt g)
        (ap G2 (pure (app (V:=C))))) <⋆> binddt f t1) <⋆>
binddt (g ⋆7 f) t2

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
map (ap G2)
  (pure
     (precompose (binddt g)
        (ap G2 (pure (app (V:=C))))) <⋆> binddt f t1) <⋆>
map (binddt g) (binddt f t2)

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
map (compose (ap G2))
  (pure
     (precompose (binddt g)
        (ap G2 (pure (app (V:=C)))))) <⋆> binddt f t1 <⋆>
map (binddt g) (binddt f t2)

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
pure
  (ap G2
   ∘ precompose (binddt g) (ap G2 (pure (app (V:=C))))) <⋆>
binddt f t1 <⋆> map (binddt g) (binddt f t2)

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
map (precompose (binddt g))
  (pure
     (ap G2
      ∘ precompose (binddt g)
          (ap G2 (pure (app (V:=C))))) <⋆> binddt f t1) <⋆>
binddt f t2

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
map (compose (precompose (binddt g)))
  (pure
     (ap G2
      ∘ precompose (binddt g)
          (ap G2 (pure (app (V:=C)))))) <⋆>
binddt f t1 <⋆> binddt f t2

        
G1: Type -> Type
Map_G: Map G1
Pure_G: Pure G1
Mult_G: Mult G1
H: Applicative G1
G2: Type -> Type
Map_G0: Map G2
Pure_G0: Pure G2
Mult_G0: Mult G2
H0: Applicative G2
B, C, A: Type
t1, t2: lam A
IHt1: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t1) =
binddt (g ⋆7 f) t1
IHt2: forall (g : nat * B -> G2 (lam C))
  (f : nat * A -> G1 (lam B)),
map (binddt g) (binddt f t2) =
binddt (g ⋆7 f) t2
g: nat * B -> G2 (lam C)
f: nat * A -> G1 (lam B)
pure (compose (binddt g) ∘ app (V:=B)) <⋆> binddt f t1 <⋆>
binddt f t2 =
pure
  (precompose (binddt g)
   ∘ (ap G2
      ∘ precompose (binddt g)
          (ap G2 (pure (app (V:=C)))))) <⋆>
binddt f t1 <⋆> binddt f t2

        reflexivity.
    
forall (G1 G2 : Type -> Type) (H : Map G1)
  (H0 : Mult G1) (H1 : Pure G1) (H2 : Map G2)
  (H3 : Mult G2) (H4 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall (A B : Type) (f : nat * A -> G1 (lam B)),
ϕ (lam B) ∘ binddt f = binddt (ϕ (lam B) ∘ f)
 
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 (lam B)
ϕ (lam B) ∘ binddt f = binddt (ϕ (lam B) ∘ f)
 
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 (lam B)
t: lam A
(ϕ (lam B) ∘ binddt f) t = binddt (ϕ (lam B) ∘ f) t

      
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
f: nat * A -> G1 (lam B)
t: lam A
ϕ (lam B) (binddt f t) = binddt (ϕ (lam B) ○ f) t

      
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t: lam A
forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t) = binddt (ϕ (lam B) ○ f) t

      
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
v: A
f: nat * A -> G1 (lam B)
ϕ (lam B) (binddt f (tvar v)) =
binddt (ϕ (lam B) ○ f) (tvar v)
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t: lam A
IHt: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t) =
binddt (ϕ (lam B) ○ f) t
f: nat * A -> G1 (lam B)
ϕ (lam B) (binddt f (abs t)) =
binddt (ϕ (lam B) ○ f) (abs t)
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t1) =
binddt (ϕ (lam B) ○ f) t1
IHt2: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t2) =
binddt (ϕ (lam B) ○ f) t2
f: nat * A -> G1 (lam B)
ϕ (lam B) (binddt f (app t1 t2)) =
binddt (ϕ (lam B) ○ f) (app t1 t2)

      
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
v: A
f: nat * A -> G1 (lam B)
ϕ (lam B) (binddt f (tvar v)) =
binddt (ϕ (lam B) ○ f) (tvar v)
 reflexivity.
      
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t: lam A
IHt: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t) =
binddt (ϕ (lam B) ○ f) t
f: nat * A -> G1 (lam B)
ϕ (lam B) (binddt f (abs t)) =
binddt (ϕ (lam B) ○ f) (abs t)
 
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t: lam A
IHt: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t) =
binddt (ϕ (lam B) ○ f) t
f: nat * A -> G1 (lam B)
ϕ (lam B) (pure (abs (V:=B)) <⋆> binddt (f ⦿ 1) t) =
pure (abs (V:=B)) <⋆> binddt ((ϕ (lam B) ○ f) ⦿ 1) t

        
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t: lam A
IHt: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t) =
binddt (ϕ (lam B) ○ f) t
f: nat * A -> G1 (lam B)
ϕ (lam B -> lam B) (pure (abs (V:=B))) <⋆>
ϕ (lam B) (binddt (f ⦿ 1) t) =
pure (abs (V:=B)) <⋆> binddt ((ϕ (lam B) ○ f) ⦿ 1) t

        
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t: lam A
IHt: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t) =
binddt (ϕ (lam B) ○ f) t
f: nat * A -> G1 (lam B)
pure (abs (V:=B)) <⋆> ϕ (lam B) (binddt (f ⦿ 1) t) =
pure (abs (V:=B)) <⋆> binddt ((ϕ (lam B) ○ f) ⦿ 1) t

        
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t: lam A
IHt: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t) =
binddt (ϕ (lam B) ○ f) t
f: nat * A -> G1 (lam B)
pure (abs (V:=B)) <⋆> binddt (ϕ (lam B) ○ f ⦿ 1) t =
pure (abs (V:=B)) <⋆> binddt ((ϕ (lam B) ○ f) ⦿ 1) t

        reflexivity.
      
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t1) =
binddt (ϕ (lam B) ○ f) t1
IHt2: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t2) =
binddt (ϕ (lam B) ○ f) t2
f: nat * A -> G1 (lam B)
ϕ (lam B) (binddt f (app t1 t2)) =
binddt (ϕ (lam B) ○ f) (app t1 t2)
 
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t1) =
binddt (ϕ (lam B) ○ f) t1
IHt2: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t2) =
binddt (ϕ (lam B) ○ f) t2
f: nat * A -> G1 (lam B)
ϕ (lam B)
  (pure (app (V:=B)) <⋆> binddt f t1 <⋆> binddt f t2) =
pure (app (V:=B)) <⋆> binddt (ϕ (lam B) ○ f) t1 <⋆>
binddt (ϕ (lam B) ○ f) t2

        
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t1) =
binddt (ϕ (lam B) ○ f) t1
IHt2: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t2) =
binddt (ϕ (lam B) ○ f) t2
f: nat * A -> G1 (lam B)
ϕ (lam B -> lam B) (pure (app (V:=B)) <⋆> binddt f t1) <⋆>
ϕ (lam B) (binddt f t2) =
pure (app (V:=B)) <⋆> binddt (ϕ (lam B) ○ f) t1 <⋆>
binddt (ϕ (lam B) ○ f) t2

        
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t1) =
binddt (ϕ (lam B) ○ f) t1
IHt2: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t2) =
binddt (ϕ (lam B) ○ f) t2
f: nat * A -> G1 (lam B)
ϕ (lam B -> lam B -> lam B) (pure (app (V:=B))) <⋆>
ϕ (lam B) (binddt f t1) <⋆> ϕ (lam B) (binddt f t2) =
pure (app (V:=B)) <⋆> binddt (ϕ (lam B) ○ f) t1 <⋆>
binddt (ϕ (lam B) ○ f) t2

        
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t1) =
binddt (ϕ (lam B) ○ f) t1
IHt2: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t2) =
binddt (ϕ (lam B) ○ f) t2
f: nat * A -> G1 (lam B)
pure (app (V:=B)) <⋆> ϕ (lam B) (binddt f t1) <⋆>
ϕ (lam B) (binddt f t2) =
pure (app (V:=B)) <⋆> binddt (ϕ (lam B) ○ f) t1 <⋆>
binddt (ϕ (lam B) ○ f) t2

        
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t1) =
binddt (ϕ (lam B) ○ f) t1
IHt2: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t2) =
binddt (ϕ (lam B) ○ f) t2
f: nat * A -> G1 (lam B)
pure (app (V:=B)) <⋆> binddt (ϕ (lam B) ○ f) t1 <⋆>
ϕ (lam B) (binddt f t2) =
pure (app (V:=B)) <⋆> binddt (ϕ (lam B) ○ f) t1 <⋆>
binddt (ϕ (lam B) ○ f) t2

        
G1, G2: Type -> Type
H: Map G1
H0: Mult G1
H1: Pure G1
H2: Map G2
H3: Mult G2
H4: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
morph: ApplicativeMorphism G1 G2 ϕ
A, B: Type
t1, t2: lam A
IHt1: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t1) =
binddt (ϕ (lam B) ○ f) t1
IHt2: forall f : nat * A -> G1 (lam B),
ϕ (lam B) (binddt f t2) =
binddt (ϕ (lam B) ○ f) t2
f: nat * A -> G1 (lam B)
pure (app (V:=B)) <⋆> binddt (ϕ (lam B) ○ f) t1 <⋆>
binddt (ϕ (lam B) ○ f) t2 =
pure (app (V:=B)) <⋆> binddt (ϕ (lam B) ○ f) t1 <⋆>
binddt (ϕ (lam B) ○ f) t2

        reflexivity.
Qed.

#[export] Instance Map_Lam: Map lam
  := DerivedOperations.Map_Binddt nat lam lam.
#[export] Instance Mapd_Lam: Mapd nat lam
  := DerivedOperations.Mapd_Binddt nat lam lam.
#[export] Instance Traverse_Lam: Traverse lam
  := DerivedOperations.Traverse_Binddt nat lam lam.
#[export] Instance Mapdt_Lam: Mapdt nat lam
  := DerivedOperations.Mapdt_Binddt nat lam lam.
#[export] Instance Bind_Lam: Bind lam lam
  := DerivedOperations.Bind_Binddt nat lam lam.
#[export] Instance Bindd_Lam: Bindd nat lam lam
  := DerivedOperations.Bindd_Binddt nat lam lam.
#[export] Instance Bindt_Lam: Bindt lam lam
  := DerivedOperations.Bindt_Binddt nat lam lam.
#[export] Instance ToSubset_Lam: ToSubset lam
  := ToSubset_Traverse.
#[export] Instance ToBatch_Lam: ToBatch lam
  := DerivedOperations.ToBatch_Traverse.

Import Notations.

Implicit Types (s t u v: lam nat) (x y: nat)
  (σ τ: nat -> lam nat) (ρ: nat -> nat).
Generalizable Variables s t u v x y σ τ ρ.
Create HintDb churchrosser.

Declare Custom Entry lambda.

(* Import DB.DB.Notations. *) (* Tealeaves notations *)
Import DB.AutosubstShim.Notations. (* Autosubst-like notations *)

Module Notations.
  Notation "{| e |}" :=
    e (e custom lambda at level 99).
  Notation "t1 t2" :=
    (app t1 t2) (in custom lambda at level 1, left associativity).
  Notation "\, t" :=
    (abs t) (in custom lambda at level 90,
          t custom lambda at level 99, left associativity).
  Notation "( x )" :=
    x (in custom lambda, x at level 99).
  Notation "x" :=
    x (in custom lambda at level 0, x constr at level 0).
End Notations.

Import Notations.

(* One step of beta reduction *)
Inductive step: lam nat -> lam nat -> Prop :=
| step_beta: forall tbody targ, step (app (abs tbody) targ) (subst (targ .: ret) tbody)
| step_app_l: forall u1 u2 t, step u1 u2 -> step (app u1 t) (app u2 t)
| step_app_r: forall u t1 t2, step t1 t2 -> step (app u t1) (app u t2)
| step_lam: forall u1 u2, step u1 u2 -> step (abs u1) (abs u2).

Notation "s → t" := (step s t) (at level 50).

#[export] Hint Constructors step: churchrosser.

Definition steps: relation (lam nat) := clos_refl_trans _ step.


Reflexive steps


Reflexive steps

  
forall x : lam nat, steps x x
 apply rt_refl.
Qed.


Transitive steps


Transitive steps

  
forall x y z : lam nat,
steps x y -> steps y z -> steps x z
 apply rt_trans.
Qed.

#[export] Hint Constructors clos_refl_trans: churchrosser.

Notation "t1 →* t2" := (steps t1 t2) (at level 50).


forall s1 s2 t, s1 →* s2 -> {|s1 t|} →* {|s2 t|}


forall s1 s2 t, s1 →* s2 -> {|s1 t|} →* {|s2 t|}

  
s1, s2, t: lam nat
H: s1 →* s2
{|s1 t|} →* {|s2 t|}
 
t, x, y: lam nat
H: x → y
{|x t|} →* {|y t|}
t, x: lam nat
{|x t|} →* {|x t|}
t, x, y, z: lam nat
H: clos_refl_trans (lam nat) step x y
H0: clos_refl_trans (lam nat) step y z
IHclos_refl_trans1: {|x t|} →* {|y t|}
IHclos_refl_trans2: {|y t|} →* {|z t|}
{|x t|} →* {|z t|}

  
t, x, y: lam nat
H: x → y
{|x t|} →* {|y t|}
 
t, x, y: lam nat
H: x → y
{|x t|} → {|y t|}
 
t, x, y: lam nat
H: x → y
x → y
 assumption.
  
t, x: lam nat
{|x t|} →* {|x t|}
 apply rt_refl.
  
t, x, y, z: lam nat
H: clos_refl_trans (lam nat) step x y
H0: clos_refl_trans (lam nat) step y z
IHclos_refl_trans1: {|x t|} →* {|y t|}
IHclos_refl_trans2: {|y t|} →* {|z t|}
{|x t|} →* {|z t|}
 eapply rt_trans; eassumption.
Qed.


forall s t1 t2, t1 →* t2 -> {|s t1|} →* {|s t2|}


forall s t1 t2, t1 →* t2 -> {|s t1|} →* {|s t2|}

  induction 1; unfold steps; eauto with churchrosser.
Qed.


forall t1 t2, t1 →* t2 -> {|\, t1|} →* {|\, t2|}


forall t1 t2, t1 →* t2 -> {|\, t1|} →* {|\, t2|}

  induction 1; unfold steps; eauto with churchrosser.
Qed.

#[export] Hint Resolve
  steps_app_r steps_lam steps_app_l: churchrosser.

Section rel_properties.

  Context
    (R1 R2: relation (lam nat)).

  Definition GDiamond := forall t t1 t2,
      R1 t t1 ->
      R1 t t2 ->
      exists t3, R2 t1 t3 /\ R2 t2 t3.

  Definition Diamond := forall t t1 t2,
      R1 t t1 ->
      R1 t t2 ->
      exists t3, R1 t1 t3 /\ R1 t2 t3.

End rel_properties.

Definition local_confluence: Prop := GDiamond step steps.
Definition confluence: Prop := Diamond steps.

#[export] Hint Unfold confluence local_confluence Diamond GDiamond: core.

Reserved Notation "t1 ⇒ t2" (at level 50).

Inductive par: lam nat -> lam nat -> Prop :=
| par_refl :
  `(tvar x ⇒ tvar x)
| par_app :
  `(s1 ⇒ s2 ->
    t1 ⇒ t2 ->
    {| s1 t1 |} ⇒ {| s2 t2 |})
| par_abs :
  `(s1 ⇒ s2 ->
    {|\, s1|} ⇒ {|\, s2|})
| par_beta :
  `(s1 ⇒ s2 ->
    t1 ⇒ t2 ->
    {| (\, s1) t1 |} ⇒ subst (t2 .: ret) s2)
where "t1 ⇒ t2" := (par t1 t2).


Reflexive par


Reflexive par

  
t: lam nat
t ⇒ t
 induction t; auto using par.
Qed.

Definition pars: relation (lam nat) := clos_refl_trans _ par.


Reflexive pars


Reflexive pars

  
forall x : lam nat, pars x x
 apply rt_refl.
Qed.


Transitive pars


Transitive pars

  
forall x y z : lam nat,
pars x y -> pars y z -> pars x z
 apply rt_trans.
Qed.

Notation "t1 ⇒* t2" := (pars t1 t2) (at level 50).

#[export] Hint Constructors par: churchrosser.

Relating →, →*, ⇒, and ⇒*

forall t1 t2, t1 → t2 -> t1 ⇒ t2


forall t1 t2, t1 → t2 -> t1 ⇒ t2

  
t1, t2: lam nat
Hstep: t1 → t2
t1 ⇒ t2
 
tbody, targ: lam nat
{|(\, tbody) targ|} ⇒ tbody.[targ/]
u1, u2, t: lam nat
Hstep: u1 → u2
IHHstep: u1 ⇒ u2
{|u1 t|} ⇒ {|u2 t|}
u, t1, t2: lam nat
Hstep: t1 → t2
IHHstep: t1 ⇒ t2
{|u t1|} ⇒ {|u t2|}
u1, u2: lam nat
Hstep: u1 → u2
IHHstep: u1 ⇒ u2
{|\, u1|} ⇒ {|\, u2|}

  
tbody, targ: lam nat
{|(\, tbody) targ|} ⇒ tbody.[targ/]
 
tbody, targ: lam nat
tbody ⇒ tbody
tbody, targ: lam nat
targ ⇒ targ

    
tbody, targ: lam nat
tbody ⇒ tbody
 reflexivity.
    
tbody, targ: lam nat
targ ⇒ targ
 reflexivity.
  
u1, u2, t: lam nat
Hstep: u1 → u2
IHHstep: u1 ⇒ u2
{|u1 t|} ⇒ {|u2 t|}
 
u1, u2, t: lam nat
Hstep: u1 → u2
IHHstep: u1 ⇒ u2
u1 ⇒ u2
u1, u2, t: lam nat
Hstep: u1 → u2
IHHstep: u1 ⇒ u2
t ⇒ t

    
u1, u2, t: lam nat
Hstep: u1 → u2
IHHstep: u1 ⇒ u2
u1 ⇒ u2
 assumption.
    
u1, u2, t: lam nat
Hstep: u1 → u2
IHHstep: u1 ⇒ u2
t ⇒ t
 reflexivity.
  
u, t1, t2: lam nat
Hstep: t1 → t2
IHHstep: t1 ⇒ t2
{|u t1|} ⇒ {|u t2|}
 
u, t1, t2: lam nat
Hstep: t1 → t2
IHHstep: t1 ⇒ t2
u ⇒ u
u, t1, t2: lam nat
Hstep: t1 → t2
IHHstep: t1 ⇒ t2
t1 ⇒ t2

    
u, t1, t2: lam nat
Hstep: t1 → t2
IHHstep: t1 ⇒ t2
u ⇒ u
 reflexivity.
    
u, t1, t2: lam nat
Hstep: t1 → t2
IHHstep: t1 ⇒ t2
t1 ⇒ t2
 assumption.
  
u1, u2: lam nat
Hstep: u1 → u2
IHHstep: u1 ⇒ u2
{|\, u1|} ⇒ {|\, u2|}
 
u1, u2: lam nat
Hstep: u1 → u2
IHHstep: u1 ⇒ u2
u1 ⇒ u2

    assumption.
Qed.


forall t1 t2, t1 ⇒ t2 -> t1 →* t2


forall t1 t2, t1 ⇒ t2 -> t1 →* t2

  
t1, t2: lam nat
Hstep: t1 ⇒ t2
t1 →* t2
 
x: nat
tvar x →* tvar x
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|s1 t1|} →* {|s2 t2|}
s1, s2: lam nat
Hstep: s1 ⇒ s2
IHHstep: s1 →* s2
{|\, s1|} →* {|\, s2|}
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|(\, s1) t1|} →* s2.[t2/]

  
x: nat
tvar x →* tvar x
 reflexivity.
  
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|s1 t1|} →* {|s2 t2|}
 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|s1 t1|} →* {|s1 t2|}
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|s1 t2|} →* {|s2 t2|}

    
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|s1 t1|} →* {|s1 t2|}
 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
t1 →* t2

      assumption.
    
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|s1 t2|} →* {|s2 t2|}
 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
s1 →* s2

      assumption.
  
s1, s2: lam nat
Hstep: s1 ⇒ s2
IHHstep: s1 →* s2
{|\, s1|} →* {|\, s2|}
 
s1, s2: lam nat
Hstep: s1 ⇒ s2
IHHstep: s1 →* s2
s1 →* s2

    assumption.
  
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|(\, s1) t1|} →* s2.[t2/]
 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|(\, s1) t1|} →* {|(\, s1) t2|}
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|(\, s1) t2|} →* s2.[t2/]

    
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|(\, s1) t1|} →* {|(\, s1) t2|}
 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
t1 →* t2

      assumption.
    
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|(\, s1) t2|} →* s2.[t2/]
 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|(\, s1) t2|} →* {|(\, s2) t2|}
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|(\, s2) t2|} →* s2.[t2/]

      
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|(\, s1) t2|} →* {|(\, s2) t2|}
 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|\, s1|} →* {|\, s2|}

        
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
s1 →* s2

        assumption.
      
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|(\, s2) t2|} →* s2.[t2/]
 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: s1 →* s2
IHHstep2: t1 →* t2
{|(\, s2) t2|} → s2.[t2/]
 apply step_beta.
Qed.


forall t1 t2, t1 ⇒* t2 -> t1 →* t2


forall t1 t2, t1 ⇒* t2 -> t1 →* t2

  
x, y: lam nat
H: x ⇒ y
x →* y
x: lam nat
x →* x
x, y, z: lam nat
H: clos_refl_trans (lam nat) par x y
H0: clos_refl_trans (lam nat) par y z
IHclos_refl_trans1: x →* y
IHclos_refl_trans2: y →* z
x →* z
 
x: lam nat
x →* x
x, y, z: lam nat
H: clos_refl_trans (lam nat) par x y
H0: clos_refl_trans (lam nat) par y z
IHclos_refl_trans1: x →* y
IHclos_refl_trans2: y →* z
x →* z

  
x, y, z: lam nat
H: clos_refl_trans (lam nat) par x y
H0: clos_refl_trans (lam nat) par y z
IHclos_refl_trans1: x →* y
IHclos_refl_trans2: y →* z
x →* z
 etransitivity; eauto.
Qed.


forall t1 t2, t1 →* t2 -> t1 ⇒* t2


forall t1 t2, t1 →* t2 -> t1 ⇒* t2

  
t1, t2: lam nat
Hstep: t1 →* t2
t1 ⇒* t2
 
x, y: lam nat
H: x → y
x ⇒* y
x: lam nat
x ⇒* x
x, y, z: lam nat
Hstep1: clos_refl_trans (lam nat) step x y
Hstep2: clos_refl_trans (lam nat) step y z
IHHstep1: x ⇒* y
IHHstep2: y ⇒* z
x ⇒* z

  
x, y: lam nat
H: x → y
x ⇒* y
 
x, y: lam nat
H: x → y
x ⇒ y
 now apply step_in_par.
  
x: lam nat
x ⇒* x
 reflexivity.
  
x, y, z: lam nat
Hstep1: clos_refl_trans (lam nat) step x y
Hstep2: clos_refl_trans (lam nat) step y z
IHHstep1: x ⇒* y
IHHstep2: y ⇒* z
x ⇒* z
 
x, y, z: lam nat
Hstep1: clos_refl_trans (lam nat) step x y
Hstep2: clos_refl_trans (lam nat) step y z
IHHstep1: x ⇒* y
IHHstep2: y ⇒* z
x ⇒* ?y
x, y, z: lam nat
Hstep1: clos_refl_trans (lam nat) step x y
Hstep2: clos_refl_trans (lam nat) step y z
IHHstep1: x ⇒* y
IHHstep2: y ⇒* z
?y ⇒* z

    
x, y, z: lam nat
Hstep1: clos_refl_trans (lam nat) step x y
Hstep2: clos_refl_trans (lam nat) step y z
IHHstep1: x ⇒* y
IHHstep2: y ⇒* z
x ⇒* ?y
 eassumption.
    
x, y, z: lam nat
Hstep1: clos_refl_trans (lam nat) step x y
Hstep2: clos_refl_trans (lam nat) step y z
IHHstep1: x ⇒* y
IHHstep2: y ⇒* z
y ⇒* z
 assumption.
Qed.


forall t1 t2, t1 → t2 -> t1 ⇒ t2


forall t1 t2, t1 → t2 -> t1 ⇒ t2

  induction 1; now constructor.
Qed.

#[export] Hint Resolve step_in_par: churchrosser.


forall t1 t2, t1 ⇒ t2 -> t1 →* t2


forall t1 t2, t1 ⇒ t2 -> t1 →* t2

  
x: nat
tvar x →* tvar x
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s1 →* s2
IHpar2: t1 →* t2
{|s1 t1|} →* {|s2 t2|}
s1, s2: lam nat
H: s1 ⇒ s2
IHpar: s1 →* s2
{|\, s1|} →* {|\, s2|}
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s1 →* s2
IHpar2: t1 →* t2
{|(\, s1) t1|} →* s2.[t2/]

  
x: nat
tvar x →* tvar x
 reflexivity.
  
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s1 →* s2
IHpar2: t1 →* t2
{|s1 t1|} →* {|s2 t2|}
 etransitivity...
  
s1, s2: lam nat
H: s1 ⇒ s2
IHpar: s1 →* s2
{|\, s1|} →* {|\, s2|}
 idtac...
  
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s1 →* s2
IHpar2: t1 →* t2
{|(\, s1) t1|} →* s2.[t2/]
 
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s1 →* s2
IHpar2: t1 →* t2
{|(\, s2) t1|} →* s2.[t2/]

    
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s1 →* s2
IHpar2: t1 →* t2
{|(\, s2) t2|} →* s2.[t2/]

    
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s1 →* s2
IHpar2: t1 →* t2
clos_refl_trans (lam nat) step {|(\, s2) t2|} s2.[t2/]

    etransitivity...
Qed.


forall t1 t2, t1 →* t2 -> t1 ⇒* t2


forall t1 t2, t1 →* t2 -> t1 ⇒* t2

  induction 1; unfold pars; eauto with churchrosser.
Qed.


forall t1 t2, t1 ⇒* t2 -> t1 →* t2


forall t1 t2, t1 ⇒* t2 -> t1 →* t2

  
x, y: lam nat
H: x ⇒ y
clos_refl_trans (lam nat) step x y

  
x, y: lam nat
H: x ⇒ y
x ⇒* y
 unfold pars...
Qed.

Notation "σ1 ▷ σ2" := (forall x, σ1 x ⇒ σ2 x) (at level 50).

Tactic Notation "asimpl" := simplify_db_like_autosubst.


forall s t, s ⇒ t -> forall σ, s.[σ] ⇒ t.[σ]


forall s t, s ⇒ t -> forall σ, s.[σ] ⇒ t.[σ]

  
s, t: lam nat
Hstep: s ⇒ t
forall σ, s.[σ] ⇒ t.[σ]

  
x: nat
σ: nat -> lam nat
(tvar x).[σ] ⇒ (tvar x).[σ]
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ, s1.[σ] ⇒ s2.[σ]
IHHstep2: forall σ, t1.[σ] ⇒ t2.[σ]
σ: nat -> lam nat
{|s1 t1|}.[σ] ⇒ {|s2 t2|}.[σ]
s1, s2: lam nat
Hstep: s1 ⇒ s2
IHHstep: forall σ, s1.[σ] ⇒ s2.[σ]
σ: nat -> lam nat
{|\, s1|}.[σ] ⇒ {|\, s2|}.[σ]
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ, s1.[σ] ⇒ s2.[σ]
IHHstep2: forall σ, t1.[σ] ⇒ t2.[σ]
σ: nat -> lam nat
{|(\, s1) t1|}.[σ] ⇒ s2.[t2/].[σ]

  
x: nat
σ: nat -> lam nat
(tvar x).[σ] ⇒ (tvar x).[σ]
 
x: nat
σ: nat -> lam nat
σ x ⇒ σ x
 reflexivity.
  
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ, s1.[σ] ⇒ s2.[σ]
IHHstep2: forall σ, t1.[σ] ⇒ t2.[σ]
σ: nat -> lam nat
{|s1 t1|}.[σ] ⇒ {|s2 t2|}.[σ]
 asimpl...
  
s1, s2: lam nat
Hstep: s1 ⇒ s2
IHHstep: forall σ, s1.[σ] ⇒ s2.[σ]
σ: nat -> lam nat
{|\, s1|}.[σ] ⇒ {|\, s2|}.[σ]
 asimpl...
  
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ, s1.[σ] ⇒ s2.[σ]
IHHstep2: forall σ, t1.[σ] ⇒ t2.[σ]
σ: nat -> lam nat
{|(\, s1) t1|}.[σ] ⇒ s2.[t2/].[σ]
 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ, s1.[σ] ⇒ s2.[σ]
IHHstep2: forall σ, t1.[σ] ⇒ t2.[σ]
σ: nat -> lam nat
{|(\, (s1.[ret 0 .: σ >>> subst ((+1) >>> ret)]))
  (t1.[σ])|} ⇒ s2.[t2.[σ] .: σ]

    
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ, s1.[σ] ⇒ s2.[σ]
IHHstep2: forall σ, t1.[σ] ⇒ t2.[σ]
σ: nat -> lam nat
{|(\, (s1.[ret 0 .: σ >>> subst ((+1) >>> ret)]))
  (t1.[σ])|} ⇒ s2.[up__sub σ].[t2.[σ]/]

    
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ, s1.[σ] ⇒ s2.[σ]
IHHstep2: forall σ, t1.[σ] ⇒ t2.[σ]
σ: nat -> lam nat
s1.[ret 0 .: σ >>> subst ((+1) >>> ret)]
⇒ s2.[up__sub σ]

    asimpl...
Qed.


forall t1 t2 ρ, t1 ⇒ t2 -> rename ρ t1 ⇒ rename ρ t2


forall t1 t2 ρ, t1 ⇒ t2 -> rename ρ t1 ⇒ rename ρ t2

  
t1, t2: lam nat
ρ: nat -> nat
H: t1 ⇒ t2
rename ρ t1 ⇒ rename ρ t2

  
t1, t2: lam nat
ρ: nat -> nat
H: t1 ⇒ t2
t1.[ρ >>> ret] ⇒ t2.[ρ >>> ret]

  
t1, t2: lam nat
H: t1 ⇒ t2
forall ρ, t1.[ρ >>> ret] ⇒ t2.[ρ >>> ret]

  
x: nat
ρ: nat -> nat
(tvar x).[ρ >>> ret] ⇒ (tvar x).[ρ >>> ret]
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: forall ρ, s1.[ρ >>> ret] ⇒ s2.[ρ >>> ret]
IHpar2: forall ρ, t1.[ρ >>> ret] ⇒ t2.[ρ >>> ret]
ρ: nat -> nat
{|s1 t1|}.[ρ >>> ret] ⇒ {|s2 t2|}.[ρ >>> ret]
s1, s2: lam nat
H: s1 ⇒ s2
IHpar: forall ρ, s1.[ρ >>> ret] ⇒ s2.[ρ >>> ret]
ρ: nat -> nat
{|\, s1|}.[ρ >>> ret] ⇒ {|\, s2|}.[ρ >>> ret]
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: forall ρ, s1.[ρ >>> ret] ⇒ s2.[ρ >>> ret]
IHpar2: forall ρ, t1.[ρ >>> ret] ⇒ t2.[ρ >>> ret]
ρ: nat -> nat
{|(\, s1) t1|}.[ρ >>> ret] ⇒ s2.[t2/].[ρ >>> ret]

  
x: nat
ρ: nat -> nat
(tvar x).[ρ >>> ret] ⇒ (tvar x).[ρ >>> ret]
 reflexivity.
  
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: forall ρ, s1.[ρ >>> ret] ⇒ s2.[ρ >>> ret]
IHpar2: forall ρ, t1.[ρ >>> ret] ⇒ t2.[ρ >>> ret]
ρ: nat -> nat
{|s1 t1|}.[ρ >>> ret] ⇒ {|s2 t2|}.[ρ >>> ret]
 asimpl...
  
s1, s2: lam nat
H: s1 ⇒ s2
IHpar: forall ρ, s1.[ρ >>> ret] ⇒ s2.[ρ >>> ret]
ρ: nat -> nat
{|\, s1|}.[ρ >>> ret] ⇒ {|\, s2|}.[ρ >>> ret]
 
s1, s2: lam nat
H: s1 ⇒ s2
IHpar: forall ρ, s1.[ρ >>> ret] ⇒ s2.[ρ >>> ret]
ρ: nat -> nat
{|\, (s1.[0 .: ρ >>> (+1) >>> ret])|}
⇒ {|\, (s2.[0 .: ρ >>> (+1) >>> ret])|}

    eauto with churchrosser.
  
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: forall ρ, s1.[ρ >>> ret] ⇒ s2.[ρ >>> ret]
IHpar2: forall ρ, t1.[ρ >>> ret] ⇒ t2.[ρ >>> ret]
ρ: nat -> nat
{|(\, s1) t1|}.[ρ >>> ret] ⇒ s2.[t2/].[ρ >>> ret]
 
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: forall ρ, s1.[ρ >>> ret] ⇒ s2.[ρ >>> ret]
IHpar2: forall ρ, t1.[ρ >>> ret] ⇒ t2.[ρ >>> ret]
ρ: nat -> nat
(rename (up__ren ρ) s1 ⇒ rename (up__ren ρ) s2 ->
 rename ρ t1 ⇒ rename ρ t2 ->
 {|(\, (rename (up__ren ρ) s1)) (rename ρ t1)|}
 ⇒ (rename (up__ren ρ) s2).[
 rename ρ t2/]) ->
{|(\, s1) t1|}.[ρ >>> ret] ⇒ s2.[t2/].[ρ >>> ret]

    asimpl...
Qed.


forall σ1 σ2, σ1 ▷ σ2 -> up__sub σ1 ▷ up__sub σ2


forall σ1 σ2, σ1 ▷ σ2 -> up__sub σ1 ▷ up__sub σ2

  
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
up__sub σ1 x ⇒ up__sub σ2 x
 
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
up__sub σ1 0 ⇒ up__sub σ2 0
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
IHx: up__sub σ1 x ⇒ up__sub σ2 x
up__sub σ1 (S x) ⇒ up__sub σ2 (S x)

  
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
up__sub σ1 0 ⇒ up__sub σ2 0
 reflexivity.
  
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
IHx: up__sub σ1 x ⇒ up__sub σ2 x
up__sub σ1 (S x) ⇒ up__sub σ2 (S x)
 
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
IHx: up__sub σ1 x ⇒ up__sub σ2 x
H0: rename (+1) (σ1 x) ⇒ rename (+1) (σ2 x)
up__sub σ1 (S x) ⇒ up__sub σ2 (S x)
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
IHx: up__sub σ1 x ⇒ up__sub σ2 x
rename (+1) (σ1 x) ⇒ rename (+1) (σ2 x)

    
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
IHx: up__sub σ1 x ⇒ up__sub σ2 x
H0: rename (+1) (σ1 x) ⇒ rename (+1) (σ2 x)
(ret 0 .: σ1 >>> subst ((+1) >>> ret)) (S x)
⇒ (ret 0 .: σ2 >>> subst ((+1) >>> ret)) (S x)
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
IHx: up__sub σ1 x ⇒ up__sub σ2 x
rename (+1) (σ1 x) ⇒ rename (+1) (σ2 x)

    
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
IHx: up__sub σ1 x ⇒ up__sub σ2 x
H0: (σ1 x).[(+1) >>> ret] ⇒ (σ2 x).[(+1) >>> ret]
(ret 0 .: σ1 >>> subst ((+1) >>> ret)) (S x)
⇒ (ret 0 .: σ2 >>> subst ((+1) >>> ret)) (S x)
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
IHx: up__sub σ1 x ⇒ up__sub σ2 x
rename (+1) (σ1 x) ⇒ rename (+1) (σ2 x)

    
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
IHx: up__sub σ1 x ⇒ up__sub σ2 x
H0: (σ1 x).[(+1) >>> ret] ⇒ (σ2 x).[(+1) >>> ret]
(σ1 >>> subst ((+1) >>> ret)) x
⇒ (σ2 >>> subst ((+1) >>> ret)) x
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
IHx: up__sub σ1 x ⇒ up__sub σ2 x
rename (+1) (σ1 x) ⇒ rename (+1) (σ2 x)
 
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
IHx: up__sub σ1 x ⇒ up__sub σ2 x
rename (+1) (σ1 x) ⇒ rename (+1) (σ2 x)

    
σ1, σ2: nat -> lam nat
H: σ1 ▷ σ2
x: nat
IHx: up__sub σ1 x ⇒ up__sub σ2 x
σ1 x ⇒ σ2 x

    apply H.
Qed.


s, t: lam nat
σ1, σ2: nat -> lam nat
s ⇒ t -> σ1 ▷ σ2 -> s.[σ1] ⇒ t.[σ2]


s, t: lam nat
σ1, σ2: nat -> lam nat
s ⇒ t -> σ1 ▷ σ2 -> s.[σ1] ⇒ t.[σ2]

  
s, t: lam nat
σ1, σ2: nat -> lam nat
Hstep: s ⇒ t
σ1 ▷ σ2 -> s.[σ1] ⇒ t.[σ2]

  
s, t: lam nat
σ2: nat -> lam nat
Hstep: s ⇒ t
forall σ1, σ1 ▷ σ2 -> s.[σ1] ⇒ t.[σ2]

  
s, t: lam nat
Hstep: s ⇒ t
forall σ2 σ1, σ1 ▷ σ2 -> s.[σ1] ⇒ t.[σ2]

  
x: nat
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
(tvar x).[σ1] ⇒ (tvar x).[σ2]
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
{|s1 t1|}.[σ1] ⇒ {|s2 t2|}.[σ2]
s1, s2: lam nat
Hstep: s1 ⇒ s2
IHHstep: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
{|\, s1|}.[σ1] ⇒ {|\, s2|}.[σ2]
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
{|(\, s1) t1|}.[σ1] ⇒ s2.[t2/].[σ2]

  
x: nat
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
(tvar x).[σ1] ⇒ (tvar x).[σ2]
 asimpl...
  
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
{|s1 t1|}.[σ1] ⇒ {|s2 t2|}.[σ2]
 asimpl...
  
s1, s2: lam nat
Hstep: s1 ⇒ s2
IHHstep: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
{|\, s1|}.[σ1] ⇒ {|\, s2|}.[σ2]
 
s1, s2: lam nat
Hstep: s1 ⇒ s2
IHHstep: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
{|\, (s1.[ret 0 .: σ1 >>> subst ((+1) >>> ret)])|}
⇒ {|\, (s2.[ret 0 .: σ2 >>> subst ((+1) >>> ret)])|}

    
s1, s2: lam nat
Hstep: s1 ⇒ s2
IHHstep: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
s1.[ret 0 .: σ1 >>> subst ((+1) >>> ret)]
⇒ s2.[ret 0 .: σ2 >>> subst ((+1) >>> ret)]

    
s1, s2: lam nat
Hstep: s1 ⇒ s2
IHHstep: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
(ret 0 .: σ1 >>> subst ((+1) >>> ret))
▷ (ret 0 .: σ2 >>> subst ((+1) >>> ret))

    
s1, s2: lam nat
Hstep: s1 ⇒ s2
IHHstep: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
up__sub σ1 ▷ up__sub σ2 ->
(ret 0 .: σ1 >>> subst ((+1) >>> ret))
▷ (ret 0 .: σ2 >>> subst ((+1) >>> ret))

    
s1, s2: lam nat
Hstep: s1 ⇒ s2
IHHstep: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
(ret 0 .: σ1 >>> subst ((+1) >>> ret))
▷ (ret 0 .: σ2 >>> subst ((+1) >>> ret)) ->
(ret 0 .: σ1 >>> subst ((+1) >>> ret))
▷ (ret 0 .: σ2 >>> subst ((+1) >>> ret))
 auto.
  
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
{|(\, s1) t1|}.[σ1] ⇒ s2.[t2/].[σ2]
 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
{|(\, (s1.[ret 0 .: σ1 >>> subst ((+1) >>> ret)]))
  (t1.[σ1])|} ⇒ s2.[t2.[σ2] .: σ2]

    
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
{|(\, (s1.[ret 0 .: σ1 >>> subst ((+1) >>> ret)]))
  (t1.[σ1])|} ⇒ s2.[up__sub σ2].[t2.[σ2]/]
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
s2.[up__sub σ2].[t2.[σ2]/] = s2.[t2.[σ2] .: σ2]

    
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
{|(\, (s1.[ret 0 .: σ1 >>> subst ((+1) >>> ret)]))
  (t1.[σ1])|} ⇒ s2.[up__sub σ2].[t2.[σ2]/]
 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
s1.[ret 0 .: σ1 >>> subst ((+1) >>> ret)]
⇒ s2.[up__sub σ2]
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
t1.[σ1] ⇒ t2.[σ2]

      
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
(ret 0 .: σ1 >>> subst ((+1) >>> ret)) ▷ up__sub σ2
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
t1.[σ1] ⇒ t2.[σ2]

      
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
up__sub σ1 ▷ up__sub σ2 ->
(ret 0 .: σ1 >>> subst ((+1) >>> ret)) ▷ up__sub σ2
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
t1.[σ1] ⇒ t2.[σ2]

      
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
t1.[σ1] ⇒ t2.[σ2]

      auto. 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
s2.[up__sub σ2].[t2.[σ2]/] = s2.[t2.[σ2] .: σ2]

    
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
s2.[up__sub σ2].[t2.[σ2]/] = s2.[t2.[σ2] .: σ2]
 
s1, s2, t1, t2: lam nat
Hstep1: s1 ⇒ s2
Hstep2: t1 ⇒ t2
IHHstep1: forall σ2 σ1, σ1 ▷ σ2 -> s1.[σ1] ⇒ s2.[σ2]
IHHstep2: forall σ2 σ1, σ1 ▷ σ2 -> t1.[σ1] ⇒ t2.[σ2]
σ2, σ1: nat -> lam nat
Hsub: σ1 ▷ σ2
s2.[(t2.[σ2] .: ret) 0 .: σ2] = s2.[t2.[σ2] .: σ2]

      reflexivity. }
Qed.

Normalization for par

Fixpoint normalize (t: lam nat): lam nat :=
  match t with
  | tvar x => tvar x
  | abs s => abs (normalize s)
  | app (abs t1) t2 => (normalize t1).[normalize t2/]
  | app t1 t2 => app (normalize t1) (normalize t2)
  end.


forall t1 t2, t1 ⇒ t2 -> t2 ⇒ normalize t1


forall t1 t2, t1 ⇒ t2 -> t2 ⇒ normalize t1

  
t1, t2: lam nat
H: t1 ⇒ t2
t2 ⇒ normalize t1
 
t1: lam nat
forall t2, t1 ⇒ t2 -> t2 ⇒ normalize t1
 
x: nat
tvar x ⇒ normalize (tvar x)
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize s1
IHpar2: t2 ⇒ normalize t1
{|s2 t2|} ⇒ normalize {|s1 t1|}
s1, s2: lam nat
H: s1 ⇒ s2
IHpar: s2 ⇒ normalize s1
{|\, s2|} ⇒ normalize {|\, s1|}
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize s1
IHpar2: t2 ⇒ normalize t1
s2.[t2/] ⇒ normalize {|(\, s1) t1|}

  
x: nat
tvar x ⇒ normalize (tvar x)
 reflexivity.
  
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize s1
IHpar2: t2 ⇒ normalize t1
{|s2 t2|} ⇒ normalize {|s1 t1|}
 
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize s1
IHpar2: t2 ⇒ normalize t1
{|s2 t2|}
⇒ match s1 with
  | {|\, t2|} => (normalize t2).[normalize t1/]
  | _ => {|(normalize s1) (normalize t1)|}
  end

    
n: nat
s2, t1, t2: lam nat
H: tvar n ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize (tvar n)
IHpar2: t2 ⇒ normalize t1
{|s2 t2|} ⇒ {|(normalize (tvar n)) (normalize t1)|}
s1, s2, t1, t2: lam nat
H: {|\, s1|} ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize {|\, s1|}
IHpar2: t2 ⇒ normalize t1
{|s2 t2|} ⇒ (normalize s1).[normalize t1/]
s1_1, s1_2, s2, t1, t2: lam nat
H: {|s1_1 s1_2|} ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize {|s1_1 s1_2|}
IHpar2: t2 ⇒ normalize t1
{|s2 t2|}
⇒ {|(normalize {|s1_1 s1_2|}) (normalize t1)|}

    
n: nat
s2, t1, t2: lam nat
H: tvar n ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize (tvar n)
IHpar2: t2 ⇒ normalize t1
{|s2 t2|} ⇒ {|(normalize (tvar n)) (normalize t1)|}
 auto using par_app.
    
s1, s2, t1, t2: lam nat
H: {|\, s1|} ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize {|\, s1|}
IHpar2: t2 ⇒ normalize t1
{|s2 t2|} ⇒ (normalize s1).[normalize t1/]
 
s1, s2, t1, t2: lam nat
H: {|\, s1|} ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize {|\, s1|}
IHpar2: t2 ⇒ normalize t1
s0, s3: lam nat
H2: s1 ⇒ s3
H1: s0 = s1
H3: {|\, s3|} = s2
{|(\, s3) t2|} ⇒ (normalize s1).[normalize t1/]
 
s1, t1, t2, s3: lam nat
H: {|\, s1|} ⇒ {|\, s3|}
H0: t1 ⇒ t2
IHpar1: {|\, s3|} ⇒ normalize {|\, s1|}
IHpar2: t2 ⇒ normalize t1
H2: s1 ⇒ s3
{|(\, s3) t2|} ⇒ (normalize s1).[normalize t1/]

      
s1, t1, t2, s3: lam nat
H: {|\, s1|} ⇒ {|\, s3|}
H0: t1 ⇒ t2
IHpar1: {|\, s3|} ⇒ normalize {|\, s1|}
IHpar2: t2 ⇒ normalize t1
H2: s1 ⇒ s3
s0, s2: lam nat
H4: s3 ⇒ normalize s1
H1: s0 = s3
H3: s2 = normalize s1
{|(\, s3) t2|} ⇒ (normalize s1).[normalize t1/]
 
s1, t1, t2, s3: lam nat
H: {|\, s1|} ⇒ {|\, s3|}
H0: t1 ⇒ t2
IHpar1: {|\, s3|} ⇒ normalize {|\, s1|}
IHpar2: t2 ⇒ normalize t1
H2: s1 ⇒ s3
H4: s3 ⇒ normalize s1
{|(\, s3) t2|} ⇒ (normalize s1).[normalize t1/]

      auto using par_beta.
    
s1_1, s1_2, s2, t1, t2: lam nat
H: {|s1_1 s1_2|} ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize {|s1_1 s1_2|}
IHpar2: t2 ⇒ normalize t1
{|s2 t2|}
⇒ {|(normalize {|s1_1 s1_2|}) (normalize t1)|}
 auto using par_app.
  
s1, s2: lam nat
H: s1 ⇒ s2
IHpar: s2 ⇒ normalize s1
{|\, s2|} ⇒ normalize {|\, s1|}
 
s1, s2: lam nat
H: s1 ⇒ s2
IHpar: s2 ⇒ normalize s1
{|\, s2|} ⇒ {|\, (normalize s1)|}
 auto using par_abs.
  
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize s1
IHpar2: t2 ⇒ normalize t1
s2.[t2/] ⇒ normalize {|(\, s1) t1|}
 
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize s1
IHpar2: t2 ⇒ normalize t1
s2.[t2/] ⇒ (normalize s1).[normalize t1/]
 
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize s1
IHpar2: t2 ⇒ normalize t1
s2 ⇒ normalize s1
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize s1
IHpar2: t2 ⇒ normalize t1
(t2 .: ret) ▷ (normalize t1 .: ret)

    
s1, s2, t1, t2: lam nat
H: s1 ⇒ s2
H0: t1 ⇒ t2
IHpar1: s2 ⇒ normalize s1
IHpar2: t2 ⇒ normalize t1
(t2 .: ret) ▷ (normalize t1 .: ret)
 now intros [|?].
Qed.


Diamond par


Diamond par

  
forall t t1 t2,
t ⇒ t1 -> t ⇒ t2 -> exists t3, t1 ⇒ t3 /\ t2 ⇒ t3
 
t, t1, t2: lam nat
H1: t ⇒ t1
H2: t ⇒ t2
exists t3, t1 ⇒ t3 /\ t2 ⇒ t3

  
t, t1, t2: lam nat
H1: t ⇒ t1
H2: t ⇒ t2
t1 ⇒ normalize t /\ t2 ⇒ normalize t
 intuition auto using par_triangle.
Qed.


forall t t1 t2,
t ⇒ t1 -> t ⇒* t2 -> exists t3, t1 ⇒* t3 /\ t2 ⇒ t3


forall t t1 t2,
t ⇒ t1 -> t ⇒* t2 -> exists t3, t1 ⇒* t3 /\ t2 ⇒ t3

  
t, t1, t2: lam nat
H1: t ⇒ t1
Hstar: t ⇒* t2
exists t3, t1 ⇒* t3 /\ t2 ⇒ t3
 
t, t2: lam nat
Hstar: t ⇒* t2
forall t1, t ⇒ t1 -> exists t3, t1 ⇒* t3 /\ t2 ⇒ t3

  
t, y: lam nat
H: t ⇒ y
t1: lam nat
H1: t ⇒ t1
exists t3, t1 ⇒* t3 /\ y ⇒ t3
t, t1: lam nat
H1: t ⇒ t1
exists t3, t1 ⇒* t3 /\ t ⇒ t3
t, y, z: lam nat
Hstar1: clos_refl_trans (lam nat) par t y
Hstar2: clos_refl_trans (lam nat) par y z
IHHstar1: forall t1,
t ⇒ t1 -> exists t3, t1 ⇒* t3 /\ y ⇒ t3
IHHstar2: forall t1,
y ⇒ t1 -> exists t3, t1 ⇒* t3 /\ z ⇒ t3
t1: lam nat
H1: t ⇒ t1
exists t3, t1 ⇒* t3 /\ z ⇒ t3

  
t, y: lam nat
H: t ⇒ y
t1: lam nat
H1: t ⇒ t1
exists t3, t1 ⇒* t3 /\ y ⇒ t3
 
t, t2: lam nat
H: t ⇒ t2
t1: lam nat
H1: t ⇒ t1
exists t3, t1 ⇒* t3 /\ t2 ⇒ t3

    
t, t2: lam nat
H: t ⇒ t2
t1: lam nat
H1: t ⇒ t1
t3: lam nat
H0: t1 ⇒ t3
H2: t2 ⇒ t3
exists t3, t1 ⇒* t3 /\ t2 ⇒ t3

    exists t3; unfold pars; split...
  
t, t1: lam nat
H1: t ⇒ t1
exists t3, t1 ⇒* t3 /\ t ⇒ t3
 
t, t1: lam nat
H1: t ⇒ t1
t1 ⇒* t1 /\ t ⇒ t1
 split; [reflexivity| auto].
  
t, y, z: lam nat
Hstar1: clos_refl_trans (lam nat) par t y
Hstar2: clos_refl_trans (lam nat) par y z
IHHstar1: forall t1,
t ⇒ t1 -> exists t3, t1 ⇒* t3 /\ y ⇒ t3
IHHstar2: forall t1,
y ⇒ t1 -> exists t3, t1 ⇒* t3 /\ z ⇒ t3
t1: lam nat
H1: t ⇒ t1
exists t3, t1 ⇒* t3 /\ z ⇒ t3
 
t, y, z: lam nat
Hstar1: clos_refl_trans (lam nat) par t y
Hstar2: clos_refl_trans (lam nat) par y z
IHHstar2: forall t1,
y ⇒ t1 -> exists t3, t1 ⇒* t3 /\ z ⇒ t3
t1: lam nat
H1: t ⇒ t1
t3: lam nat
H: t1 ⇒* t3
H0: y ⇒ t3
exists t3, t1 ⇒* t3 /\ z ⇒ t3

    
t, y, z: lam nat
Hstar1: clos_refl_trans (lam nat) par t y
Hstar2: clos_refl_trans (lam nat) par y z
t1: lam nat
H1: t ⇒ t1
t3: lam nat
H: t1 ⇒* t3
H0: y ⇒ t3
t4: lam nat
H2: t3 ⇒* t4
H3: z ⇒ t4
exists t3, t1 ⇒* t3 /\ z ⇒ t3

    
t, y, z: lam nat
Hstar1: clos_refl_trans (lam nat) par t y
Hstar2: clos_refl_trans (lam nat) par y z
t1: lam nat
H1: t ⇒ t1
t3: lam nat
H: t1 ⇒* t3
H0: y ⇒ t3
t4: lam nat
H2: t3 ⇒* t4
H3: z ⇒ t4
t1 ⇒* t4 /\ z ⇒ t4
 split; [etransitivity; eauto| assumption].
Qed.


Diamond pars


Diamond pars

  
forall t t1 t2,
t ⇒* t1 -> t ⇒* t2 -> exists t3, t1 ⇒* t3 /\ t2 ⇒* t3
 
t, t1, t2: lam nat
Ht1: t ⇒* t1
Ht2: t ⇒* t2
exists t3, t1 ⇒* t3 /\ t2 ⇒* t3

  
t, t1: lam nat
Ht1: t ⇒* t1
forall t2, t ⇒* t2 -> exists t3, t1 ⇒* t3 /\ t2 ⇒* t3
 
x, y: lam nat
H: x ⇒ y
t2: lam nat
Ht2: x ⇒* t2
exists t3, y ⇒* t3 /\ t2 ⇒* t3
x, t2: lam nat
Ht2: x ⇒* t2
exists t3, x ⇒* t3 /\ t2 ⇒* t3
x, y, z: lam nat
Ht1_1: clos_refl_trans (lam nat) par x y
Ht1_2: clos_refl_trans (lam nat) par y z
IHHt1_1: forall t2,
x ⇒* t2 -> exists t3, y ⇒* t3 /\ t2 ⇒* t3
IHHt1_2: forall t2,
y ⇒* t2 -> exists t3, z ⇒* t3 /\ t2 ⇒* t3
t2: lam nat
Ht2: x ⇒* t2
exists t3, z ⇒* t3 /\ t2 ⇒* t3

  
x, y: lam nat
H: x ⇒ y
t2: lam nat
Ht2: x ⇒* t2
exists t3, y ⇒* t3 /\ t2 ⇒* t3
 
t, y: lam nat
H: t ⇒ y
t2: lam nat
Ht2: t ⇒* t2
exists t3, y ⇒* t3 /\ t2 ⇒* t3
 
t, t1: lam nat
H: t ⇒ t1
t2: lam nat
Ht2: t ⇒* t2
exists t3, t1 ⇒* t3 /\ t2 ⇒* t3

    
t, t1: lam nat
H: t ⇒ t1
t2: lam nat
Ht2: t ⇒* t2
t3: lam nat
H0: t1 ⇒* t3
H1: t2 ⇒ t3
exists t3, t1 ⇒* t3 /\ t2 ⇒* t3

    
t, t1: lam nat
H: t ⇒ t1
t2: lam nat
Ht2: t ⇒* t2
t3: lam nat
H0: t1 ⇒* t3
H1: t2 ⇒ t3
t1 ⇒* t3 /\ t2 ⇒* t3
 
t, t1: lam nat
H: t ⇒ t1
t2: lam nat
Ht2: clos_refl_trans (lam nat) par t t2
t3: lam nat
H0: clos_refl_trans (lam nat) par t1 t3
H1: t2 ⇒ t3
clos_refl_trans (lam nat) par t1 t3 /\
clos_refl_trans (lam nat) par t2 t3
 split; auto with churchrosser.
  
x, t2: lam nat
Ht2: x ⇒* t2
exists t3, x ⇒* t3 /\ t2 ⇒* t3
 
x, t2: lam nat
Ht2: x ⇒* t2
x ⇒* t2 /\ t2 ⇒* t2
 
x, t2: lam nat
Ht2: clos_refl_trans (lam nat) par x t2
clos_refl_trans (lam nat) par x t2 /\
clos_refl_trans (lam nat) par t2 t2
 split; auto with churchrosser.
  
x, y, z: lam nat
Ht1_1: clos_refl_trans (lam nat) par x y
Ht1_2: clos_refl_trans (lam nat) par y z
IHHt1_1: forall t2,
x ⇒* t2 -> exists t3, y ⇒* t3 /\ t2 ⇒* t3
IHHt1_2: forall t2,
y ⇒* t2 -> exists t3, z ⇒* t3 /\ t2 ⇒* t3
t2: lam nat
Ht2: x ⇒* t2
exists t3, z ⇒* t3 /\ t2 ⇒* t3
 
x, y, z: lam nat
Ht1_1: clos_refl_trans (lam nat) par x y
Ht1_2: clos_refl_trans (lam nat) par y z
IHHt1_1: forall t2,
x ⇒* t2 -> exists t3, y ⇒* t3 /\ t2 ⇒* t3
IHHt1_2: forall t2,
y ⇒* t2 -> exists t3, z ⇒* t3 /\ t2 ⇒* t3
t2: lam nat
Ht2: x ⇒* t2
t3: lam nat
H: y ⇒* t3
H0: t2 ⇒* t3
exists t3, z ⇒* t3 /\ t2 ⇒* t3

    
x, y, z: lam nat
Ht1_1: clos_refl_trans (lam nat) par x y
Ht1_2: clos_refl_trans (lam nat) par y z
IHHt1_1: forall t2,
x ⇒* t2 -> exists t3, y ⇒* t3 /\ t2 ⇒* t3
IHHt1_2: forall t2,
y ⇒* t2 -> exists t3, z ⇒* t3 /\ t2 ⇒* t3
t2: lam nat
Ht2: x ⇒* t2
t3: lam nat
H: y ⇒* t3
H0: t2 ⇒* t3
t4: lam nat
H1: z ⇒* t4
H2: t3 ⇒* t4
exists t3, z ⇒* t3 /\ t2 ⇒* t3

    
x, y, z: lam nat
Ht1_1: clos_refl_trans (lam nat) par x y
Ht1_2: clos_refl_trans (lam nat) par y z
IHHt1_1: forall t2,
x ⇒* t2 -> exists t3, y ⇒* t3 /\ t2 ⇒* t3
IHHt1_2: forall t2,
y ⇒* t2 -> exists t3, z ⇒* t3 /\ t2 ⇒* t3
t2: lam nat
Ht2: x ⇒* t2
t3: lam nat
H: y ⇒* t3
H0: t2 ⇒* t3
t4: lam nat
H1: z ⇒* t4
H2: t3 ⇒* t4
z ⇒* t4 /\ t2 ⇒* t4
 
x, y, z: lam nat
Ht1_1: clos_refl_trans (lam nat) par x y
Ht1_2: clos_refl_trans (lam nat) par y z
IHHt1_1: forall t2,
x ⇒* t2 -> exists t3, y ⇒* t3 /\ t2 ⇒* t3
IHHt1_2: forall t2,
y ⇒* t2 -> exists t3, z ⇒* t3 /\ t2 ⇒* t3
t2: lam nat
Ht2: x ⇒* t2
t3: lam nat
H: y ⇒* t3
H0: t2 ⇒* t3
t4: lam nat
H1: z ⇒* t4
H2: t3 ⇒* t4
z ⇒* t4
x, y, z: lam nat
Ht1_1: clos_refl_trans (lam nat) par x y
Ht1_2: clos_refl_trans (lam nat) par y z
IHHt1_1: forall t2,
x ⇒* t2 -> exists t3, y ⇒* t3 /\ t2 ⇒* t3
IHHt1_2: forall t2,
y ⇒* t2 -> exists t3, z ⇒* t3 /\ t2 ⇒* t3
t2: lam nat
Ht2: x ⇒* t2
t3: lam nat
H: y ⇒* t3
H0: t2 ⇒* t3
t4: lam nat
H1: z ⇒* t4
H2: t3 ⇒* t4
t2 ⇒* t4
 
x, y, z: lam nat
Ht1_1: clos_refl_trans (lam nat) par x y
Ht1_2: clos_refl_trans (lam nat) par y z
IHHt1_1: forall t2,
x ⇒* t2 -> exists t3, y ⇒* t3 /\ t2 ⇒* t3
IHHt1_2: forall t2,
y ⇒* t2 -> exists t3, z ⇒* t3 /\ t2 ⇒* t3
t2: lam nat
Ht2: x ⇒* t2
t3: lam nat
H: y ⇒* t3
H0: t2 ⇒* t3
t4: lam nat
H1: z ⇒* t4
H2: t3 ⇒* t4
t2 ⇒* t4
 etransitivity; eauto.
Qed.

Proving confluence of steps

confluence


confluence

  
Diamond steps
 
forall t t1 t2,
t →* t1 -> t →* t2 -> exists t3, t1 →* t3 /\ t2 →* t3
 
t, t1, t2: lam nat
H: t →* t1
H0: t →* t2
exists t3, t1 →* t3 /\ t2 →* t3

  
t, t1, t2: lam nat
H: t →* t1
H0: t →* t2
H1: t ⇒* t1
exists t3, t1 →* t3 /\ t2 →* t3

  
t, t1, t2: lam nat
H: t →* t1
H0: t →* t2
H1: t ⇒* t1
H2: t ⇒* t2
exists t3, t1 →* t3 /\ t2 →* t3

  
t, t1, t2: lam nat
H: t →* t1
H0: t →* t2
H1: t ⇒* t1
H2: t ⇒* t2
t3: lam nat
H3: t1 ⇒* t3
H4: t2 ⇒* t3
exists t3, t1 →* t3 /\ t2 →* t3
 exists t3; split; now apply pars_in_steps.
Qed.

Beta equivalence

There are a couple ways to define the notion of \(\beta\)-equivalence (a/k/a \(\beta\)-conversion or \(\beta\)-congruence). Just as steps was defined as the reflexive transitive closure of step, beta_equiv can be defined as the reflexive symmetric transitive closure of step, i.e. the smallest equivalence relation that contains step.

As with steps, the first thing we do after defining beta_equiv is prove that it is indeed reflexive, symmetric, and transitive, enabling the use of the correspondingly named tactics. We also give this relation a custom notation and add its constructors to our hint database.

Definition beta_equiv: relation (lam nat) := clos_refl_sym_trans _ step.


Reflexive beta_equiv


Reflexive beta_equiv

  
forall x : lam nat, beta_equiv x x
 apply rst_refl.
Qed.


Symmetric beta_equiv


Symmetric beta_equiv

  
forall x y : lam nat, beta_equiv x y -> beta_equiv y x
 apply rst_sym.
Qed.


Transitive beta_equiv


Transitive beta_equiv

  
forall x y z : lam nat,
beta_equiv x y -> beta_equiv y z -> beta_equiv x z
 apply rst_trans.
Qed.

Notation "s ∼ t" := (beta_equiv s t) (at level 50).

#[export] Hint Constructors clos_refl_sym_trans: churchrosser.

Beta equivalence is also called a congruence relation, meaning an equivalence relation that is respected by a set of operations, in this case the constructors of (lam nat). By "respected by the constructors of (lam nat)" I mean exactly the following three properties, much like ones we gave earlier for steps.

forall s1 s2 t, s1 ∼ s2 -> {|s1 t|} ∼ {|s2 t|}


forall s1 s2 t, s1 ∼ s2 -> {|s1 t|} ∼ {|s2 t|}

  induction 1; unfold beta_equiv; eauto with churchrosser.
Qed.


forall t1 t2 s, t1 ∼ t2 -> {|s t1|} ∼ {|s t2|}


forall t1 t2 s, t1 ∼ t2 -> {|s t1|} ∼ {|s t2|}

  induction 1; unfold beta_equiv; eauto with churchrosser.
Qed.


forall t1 t2, t1 ∼ t2 -> {|\, t1|} ∼ {|\, t2|}


forall t1 t2, t1 ∼ t2 -> {|\, t1|} ∼ {|\, t2|}

  induction 1; unfold beta_equiv; eauto with churchrosser.
Qed.

#[export] Hint Resolve
  beta_equiv_app_r beta_equiv_lam beta_equiv_app_l: churchrosser.

Axiomatization of beta equivalence

Instead of defining \(\beta\)-equivalence as the equivalence closure of step, another route is to define the relation inductively from a set of equational axioms, as shown below with beta_equiv_I.

Reserved Notation "s ≃ t" (at level 50).

Inductive beta_equiv_I: lam nat -> lam nat -> Prop :=
| equ_refl: `(s ≃ s)
| equ_sym : `(s ≃ t ->
                t ≃ s)
| equ_trans: `(s ≃ t ->
                t ≃ u ->
                s ≃ u)
| equ_beta: `({|(\, s) t|} ≃ s.[t/])
| equ_app_l: `(s1 ≃ s2 ->
                {|s1 t|} ≃ {|s2 t|})
| equ_app_r: `(t1 ≃ t2 ->
                {|s t1|} ≃ {|s t2|})
| equ_lam: `(s1 ≃ s2 ->
             {|\, s1|} ≃ {|\, s2|})
where "s ≃ t" := (beta_equiv_I s t).

#[export] Hint Constructors beta_equiv_I: churchrosser.

If you're following along in Barendregt, this definition of \(\beta\)-congruence matches Barendregt's definition of the equational theory λ (Definition 2.1.4, pg. 23). In some sense this style of definition is simpler to think about (and to generalize to other calculi) because it does not require introducing an auxiliary relation like step. This could be beneficial in situations where we know which terms we want to be equal, but it is not clear how to describe this equality in terms of reduction steps.

It is easy to show that our two definitions of beta conversion coincide.

forall s t, s ∼ t <-> s ≃ t


forall s t, s ∼ t <-> s ≃ t

  
s, t: lam nat
s ∼ t <-> s ≃ t
 
s, t: lam nat
s ∼ t -> s ≃ t
s, t: lam nat
s ≃ t -> s ∼ t

  
s, t: lam nat
s ∼ t -> s ≃ t
 
x, y: lam nat
H: x → y
x ≃ y
x, y, z: lam nat
H: clos_refl_sym_trans (lam nat) step x y
H0: clos_refl_sym_trans (lam nat) step y z
IHclos_refl_sym_trans1: x ≃ y
IHclos_refl_sym_trans2: y ≃ z
x ≃ z

    
x, y: lam nat
H: x → y
x ≃ y
 induction H...
    
x, y, z: lam nat
H: clos_refl_sym_trans (lam nat) step x y
H0: clos_refl_sym_trans (lam nat) step y z
IHclos_refl_sym_trans1: x ≃ y
IHclos_refl_sym_trans2: y ≃ z
x ≃ z
 eauto with churchrosser.
  
s, t: lam nat
s ≃ t -> s ∼ t
 
s: lam nat
s ∼ s
s, t: lam nat
H: s ≃ t
IHbeta_equiv_I: s ∼ t
t ∼ s
s, t, u: lam nat
H: s ≃ t
H0: t ≃ u
IHbeta_equiv_I1: s ∼ t
IHbeta_equiv_I2: t ∼ u
s ∼ u
s, t: lam nat
{|(\, s) t|} ∼ s.[t/]

    
s: lam nat
s ∼ s
 reflexivity.
    
s, t: lam nat
H: s ≃ t
IHbeta_equiv_I: s ∼ t
t ∼ s
 symmetry...
    
s, t, u: lam nat
H: s ≃ t
H0: t ≃ u
IHbeta_equiv_I1: s ∼ t
IHbeta_equiv_I2: t ∼ u
s ∼ u
 etransitivity; eassumption.
    
s, t: lam nat
{|(\, s) t|} ∼ s.[t/]
 unfold beta_equiv...
Qed.

Corollaries of confluence

Confluence is a pleasing technical property with a few useful corollaries. First, if we want to know whether two terms are beta-equivalent, by confluence it suffices to check whether the terms can be reduced to a common term. This is important because, at face value, deciding equivalence sounds much harder. Second, it implies that if a given lambda term t reduces to some irreducible term s, this property unique defines s. This is important because beta-reduction is non-deterministic, and the prior statement implies any reduction sequence that discovers a normal form for t must find the same normal form. In the context of typed lambda calculi that enjoy strong normalization (a separate topic), this fact implies it is decidable whether two terms are \(beta\)-equivalent. In particular, this a crucial theoretical fact underlying how Coq itself decides whether two terms are defintionally equal, a key aspect of Coq and theorem proving in general.

Transitivity of common reduct

Definition have_common_reduct: lam nat -> lam nat -> Prop :=
  fun s t => exists u, s →* u /\ t →* u.


Transitive have_common_reduct


Transitive have_common_reduct

  
forall x y z : lam nat,
have_common_reduct x y ->
have_common_reduct y z -> have_common_reduct x z
 
s, t, v, st: lam nat
H: s →* st
H0: t →* st
tv: lam nat
H1: t →* tv
H2: v →* tv
have_common_reduct s v

  
s, t, v, st: lam nat
H: s →* st
H0: t →* st
tv: lam nat
H1: t →* tv
H2: v →* tv
cut: have_common_reduct st tv
have_common_reduct s v
s, t, v, st: lam nat
H: s →* st
H0: t →* st
tv: lam nat
H1: t →* tv
H2: v →* tv
have_common_reduct st tv

  
s, t, v, st: lam nat
H: s →* st
H0: t →* st
tv: lam nat
H1: t →* tv
H2: v →* tv
cut: have_common_reduct st tv
have_common_reduct s v
 
s, t, v, st: lam nat
H: s →* st
H0: t →* st
tv: lam nat
H1: t →* tv
H2: v →* tv
cut: exists u, st →* u /\ tv →* u
exists u, s →* u /\ v →* u

    
s, t, v, st: lam nat
H: s →* st
H0: t →* st
tv: lam nat
H1: t →* tv
H2: v →* tv
u: lam nat
H3: st →* u
H4: tv →* u
exists u, s →* u /\ v →* u

    
s, t, v, st: lam nat
H: s →* st
H0: t →* st
tv: lam nat
H1: t →* tv
H2: v →* tv
u: lam nat
H3: st →* u
H4: tv →* u
s →* u /\ v →* u
 split; etransitivity; eassumption.
  
s, t, v, st: lam nat
H: s →* st
H0: t →* st
tv: lam nat
H1: t →* tv
H2: v →* tv
have_common_reduct st tv
 
s, t, v, st: lam nat
H: s →* st
H0: t →* st
tv: lam nat
H1: t →* tv
H2: v →* tv
exists u, st →* u /\ tv →* u

    
s, t, v, st: lam nat
H: s →* st
H0: t →* st
tv: lam nat
H1: t →* tv
H2: v →* tv
u: lam nat
H3: st →* u
H4: tv →* u
exists u, st →* u /\ tv →* u
 
s, t, v, st: lam nat
H: s →* st
H0: t →* st
tv: lam nat
H1: t →* tv
H2: v →* tv
u: lam nat
H3: st →* u
H4: tv →* u
st →* u /\ tv →* u
 tauto.
Qed.

Specification for beta conversion

The following specification theorem for \(\beta\)-conversion states that two terms are \(\beta\)-equivalent exactly when they share a common reduct. The non-obvious case of this proof is exactly showing the transitivity of the have_common_reduct relation. This case is unfolded below to show the proof state before invoking transitivity.

forall s t, have_common_reduct s t <-> s ∼ t


forall s t, have_common_reduct s t <-> s ∼ t

  
s, t: lam nat
have_common_reduct s t <-> s ∼ t
 
s, t: lam nat
have_common_reduct s t -> s ∼ t
s, t: lam nat
s ∼ t -> have_common_reduct s t
 
s, t, st: lam nat
H: s →* st
H0: t →* st
s ∼ t
s, t: lam nat
s ∼ t -> have_common_reduct s t

  
s, t, st: lam nat
H: s →* st
H0: t →* st
s ∼ t
 
s, t, st: lam nat
H: s →* st
H0: t →* st
s ∼ st
s, t, st: lam nat
H: s →* st
H0: t →* st
st ∼ t

    
s, t, st: lam nat
H: s →* st
H0: t →* st
s ∼ st
 
s, t, st: lam nat
H: s →* st
H0: t →* st
clos_refl_trans (lam nat) step s st

      
s, t, st: lam nat
H: s →* st
H0: t →* st
s →* st
 assumption.
    
s, t, st: lam nat
H: s →* st
H0: t →* st
st ∼ t
 
s, t, st: lam nat
H: s →* st
H0: t →* st
t ∼ st
 
s, t, st: lam nat
H: s →* st
H0: t →* st
t ∼ st

      
s, t, st: lam nat
H: s →* st
H0: t →* st
clos_refl_trans (lam nat) step t st

      
s, t, st: lam nat
H: s →* st
H0: t →* st
t →* st
 assumption.
  
s, t: lam nat
s ∼ t -> have_common_reduct s t
 
s, t: lam nat
H: s ∼ t
have_common_reduct s t
 
x, y: lam nat
H: x → y
have_common_reduct x y
x: lam nat
have_common_reduct x x
x, y: lam nat
H: clos_refl_sym_trans (lam nat) step x y
IHclos_refl_sym_trans: have_common_reduct x y
have_common_reduct y x
x, y, z: lam nat
H: clos_refl_sym_trans (lam nat) step x y
H0: clos_refl_sym_trans (lam nat) step y z
IHclos_refl_sym_trans1: have_common_reduct x y
IHclos_refl_sym_trans2: have_common_reduct y z
have_common_reduct x z

    
x, y: lam nat
H: x → y
have_common_reduct x y

      
x, y: lam nat
H: x → y
x →* y /\ y →* y
 unfold steps...
    
x: lam nat
have_common_reduct x x

      
x: lam nat
x →* x /\ x →* x
 unfold steps...
    
x, y: lam nat
H: clos_refl_sym_trans (lam nat) step x y
IHclos_refl_sym_trans: have_common_reduct x y
have_common_reduct y x

      
x, y: lam nat
H: clos_refl_sym_trans (lam nat) step x y
z: lam nat
H0: x →* z
H1: y →* z
have_common_reduct y x
 
x, y: lam nat
H: clos_refl_sym_trans (lam nat) step x y
z: lam nat
H0: x →* z
H1: y →* z
y →* z /\ x →* z
 tauto.
    
x, y, z: lam nat
H: clos_refl_sym_trans (lam nat) step x y
H0: clos_refl_sym_trans (lam nat) step y z
IHclos_refl_sym_trans1: have_common_reduct x y
IHclos_refl_sym_trans2: have_common_reduct y z
have_common_reduct x z

      etransitivity; eassumption.
Qed.

Uniqueness of normal forms

Definition beta_normal (t: lam nat): Prop :=
  not (exists s, t → s).

Definition has_normal_form (t s: lam nat): Prop :=
  t →* s /\ beta_normal s.


forall t s, beta_normal t -> t →* s -> t = s


forall t s, beta_normal t -> t →* s -> t = s

  
t, s: lam nat
Hnorm: beta_normal t
Hstep: t →* s
t = s
 
x: lam nat
Hnorm: beta_normal x
y: lam nat
H: x → y
x = y
x: lam nat
Hnorm: beta_normal x
x = x
x: lam nat
Hnorm: beta_normal x
y, z: lam nat
Hstep1: clos_refl_trans (lam nat) step x y
Hstep2: clos_refl_trans (lam nat) step y z
IHHstep1: beta_normal x -> x = y
IHHstep2: beta_normal y -> y = z
x = z

  
x: lam nat
Hnorm: beta_normal x
y: lam nat
H: x → y
x = y
 
x: lam nat
Hnorm: beta_normal x
y: lam nat
H: x → y
exists s, x → s
 eauto.
  
x: lam nat
Hnorm: beta_normal x
x = x
 reflexivity.
  
x: lam nat
Hnorm: beta_normal x
y, z: lam nat
Hstep1: clos_refl_trans (lam nat) step x y
Hstep2: clos_refl_trans (lam nat) step y z
IHHstep1: beta_normal x -> x = y
IHHstep2: beta_normal y -> y = z
x = z
 
x: lam nat
Hnorm: beta_normal x
y, z: lam nat
Hstep1: x →* y
Hstep2: y →* z
IHHstep1: beta_normal x -> x = y
IHHstep2: beta_normal y -> y = z
x = z
 
x: lam nat
Hnorm: beta_normal x
y, z: lam nat
Hstep1: x →* y
Hstep2: y →* z
IHHstep1: x = y
IHHstep2: beta_normal y -> y = z
x = z
 
y: lam nat
Hnorm: beta_normal y
z: lam nat
Hstep1: y →* y
Hstep2: y →* z
IHHstep2: beta_normal y -> y = z
y = z

    
y: lam nat
Hnorm: beta_normal y
z: lam nat
Hstep1: y →* y
Hstep2: y →* z
IHHstep2: beta_normal y -> y = z
beta_normal y
 apply Hnorm.
Qed.


forall t s1 s2,
has_normal_form t s1 ->
has_normal_form t s2 -> s1 = s2


forall t s1 s2,
has_normal_form t s1 ->
has_normal_form t s2 -> s1 = s2

  
forall t s1 s2,
t →* s1 /\ beta_normal s1 ->
t →* s2 /\ beta_normal s2 -> s1 = s2

  
t, s1, s2: lam nat
t_step_s1: t →* s1
s1_normal: beta_normal s1
t_step_s2: t →* s2
s2_normal: beta_normal s2
s1 = s2

  
t, s1, s2: lam nat
t_step_s1: t →* s1
s1_normal: beta_normal s1
t_step_s2: t →* s2
s2_normal: beta_normal s2
s: lam nat
s1_step_s: s1 →* s
s2_step_s: s2 →* s
s1 = s2

  
t, s1, s2: lam nat
t_step_s1: t →* s1
s1_normal: beta_normal s1
t_step_s2: t →* s2
s2_normal: beta_normal s2
s: lam nat
s1_step_s: s1 →* s
s2_step_s: s2 →* s
H: s1 = s
s1 = s2

  
t, s1, s2: lam nat
t_step_s1: t →* s1
s1_normal: beta_normal s1
t_step_s2: t →* s2
s2_normal: beta_normal s2
s: lam nat
s1_step_s: s1 →* s
s2_step_s: s2 →* s
H: s1 = s
H0: s2 = s
s1 = s2

  congruence.
Qed.


forall t s, t ∼ s -> beta_normal s -> t →* s


forall t s, t ∼ s -> beta_normal s -> t →* s

  
t, s: lam nat
Heq: t ∼ s
normal_s: beta_normal s
t →* s

  
t, s: lam nat
Hcr: have_common_reduct t s
normal_s: beta_normal s
t →* s

  
t, s, u: lam nat
Htu: t →* u
Hsu: s →* u
normal_s: beta_normal s
t →* s

  
t, s, u: lam nat
Htu: t →* u
Hsu: s →* u
normal_s: beta_normal s
H: s = u
t →* s

  
t, u: lam nat
Htu: t →* u
normal_s: beta_normal u
Hsu: u →* u
t →* u

  assumption.
Qed.


forall t t' s,
t →* t' -> has_normal_form t s -> has_normal_form t' s


forall t t' s,
t →* t' -> has_normal_form t s -> has_normal_form t' s

  
forall t t' s,
t →* t' ->
t →* s /\ beta_normal s -> t' →* s /\ beta_normal s

  
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
t' →* s /\ beta_normal s

  
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
t' →* s
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
beta_normal s

  
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
t' →* s
 
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
t' ∼ s
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
beta_normal s

    
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
t' ∼ s
 
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
t' ∼ t
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
t ∼ s

      
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
t' ∼ t
 
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
t ∼ t'

        
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
t →* t'

        assumption.
      
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
t ∼ s
 
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
t →* s

        assumption.
    
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
beta_normal s
 assumption.
  
t, t', s: lam nat
t_step_t': t →* t'
t_step_s: t →* s
s_normal: beta_normal s
beta_normal s
 assumption.
Qed.


forall t t', t →* t' -> t ∼ t'


forall t t', t →* t' -> t ∼ t'

  
t, t': lam nat
H: t →* t'
t ∼ t'

  
t, t': lam nat
H: t →* t'
clos_refl_trans (lam nat) step t t'

  assumption.
Qed.


forall t t' s,
t ∼ t' -> has_normal_form t s -> has_normal_form t' s


forall t t' s,
t ∼ t' -> has_normal_form t s -> has_normal_form t' s

  
forall t t' s,
t ∼ t' ->
t →* s /\ beta_normal s -> t' →* s /\ beta_normal s

  
t, t', s: lam nat
t_equiv_t': t ∼ t'
t_step_s: t →* s
normal_s: beta_normal s
t' →* s /\ beta_normal s

  
t, t', s: lam nat
t_equiv_t': t ∼ t'
t_step_s: t →* s
normal_s: beta_normal s
t' →* s

  
t, t', s: lam nat
t_equiv_t': t ∼ t'
t_step_s: t →* s
normal_s: beta_normal s
t' ∼ s

  
t, t', s: lam nat
t_equiv_t': t ∼ t'
t_step_s: t ∼ s
normal_s: beta_normal s
t' ∼ s

  etransitivity; [symmetry|]; eauto.
Qed.