From Stdlib Require Import List Bool Arith Lia PeanoNat.
Import ListNotations.
From LambdaSub Require Import ExecReducer Binding Reduction.

Inductive red_sub_root : trm -> trm -> Prop :=
| rs_gc : forall body u, occurs0 body = false -> red_sub_root (ESub body u) body
| rs_r : forall C body u, zfill C 0 = body ->
    red_sub_root (ESub body u) (ESub (zplug_lift C 0 u) u).

Inductive red_sub : trm -> trm -> Prop :=
| red_sub_base : forall t t', red_sub_root t t' -> red_sub t t'
| red_sub_ctx : forall C t t', red_sub t t' -> red_sub (plug C t) (plug C t').

Lemma red_sub_root_to_red1 : forall t t', red_sub_root t t' -> red1 t t'.
Proof.
  intros t t' H. destruct H.
  - exists RGc. apply red1r_root. apply rGc. exact H.
  - exists RR. apply red1r_root. apply rR. exact H.
Qed.

Lemma red_sub_to_red1 : forall t t', red_sub t t' -> red1 t t'.
Proof.
  intros t t' H. induction H.
  - apply red_sub_root_to_red1. exact H.
  - destruct IHred_sub as [r Hr]. exists r. apply rctx. exact Hr.
Qed.

Lemma red_sub_context : forall C t t', red_sub t t' -> red_sub (plug C t) (plug C t').
Proof. intros. apply red_sub_ctx. exact H. Qed.

Lemma red_sub_gc : forall body u, occurs0 body = false -> red_sub (ESub body u) body.
Proof. intros. apply red_sub_base. apply rs_gc. exact H. Qed.

Lemma red_sub_r : forall C body u, zfill C 0 = body ->
  red_sub (ESub body u) (ESub (zplug_lift C 0 u) u).
Proof. intros. apply red_sub_base. apply rs_r. exact H. Qed.

Print Assumptions red_sub_root_to_red1.
Print Assumptions red_sub_to_red1.
Print Assumptions red_sub_context.