From Stdlib Require Import List Bool Arith Lia PeanoNat.
From Stdlib Require Import Setoid Morphisms.
Import ListNotations.
From LambdaSub Require Import NamedMeta.

(* A setoid rewriting layer for the C equivalence Es on named metaterms.

   Es is the congruence generated by the equation C (together with the
   implicit alpha convention of the paper, which the named core does not
   quotient). We register Es as an equivalence and as a congruence for the
   term constructors and for every context, so that setoid rewriting can
   move along Es. We then define the reduction relation modulo Es (subred)
   and prove that it is stable on both sides and under every context. *)

Instance Es_Equivalence : Equivalence Es.
Proof.
  split.
  - intro t. apply Es_refl.
  - intros a b Hab. apply Es_sym. exact Hab.
  - intros a b c Hab Hbc. apply Es_trans with (u := b); assumption.
Qed.

Instance Es_NVar_Proper : Proper (eq ==> Es) NVar.
Proof. intros a b Hab. subst b. apply Es_refl. Qed.

Instance Es_NMVar_Proper : Proper (eq ==> eq ==> Es) NMVar.
Proof. intros a b Hab c d Hcd. subst b d. apply Es_refl. Qed.

Instance Es_NApp_Proper : Proper (Es ==> Es ==> Es) NApp.
Proof.
  intros a b Hab c d Hcd.
  apply Es_trans with (u := NApp b c).
  - apply Es_ctx with (C := nAppL nHole c). exact Hab.
  - apply Es_ctx with (C := nAppR b nHole). exact Hcd.
Qed.

Instance Es_NLam_Proper (x : atom) : Proper (Es ==> Es) (NLam x).
Proof. intros a b Hab. apply Es_ctx with (C := nLam x nHole). exact Hab. Qed.

Instance Es_NESub_Proper : Proper (Es ==> eq ==> Es ==> Es) NESub.
Proof.
  intros a b Hab x y Hxy c d Hcd. subst y.
  apply Es_trans with (u := NESub b x c).
  - apply Es_ctx with (C := nESubL nHole x c). exact Hab.
  - apply Es_ctx with (C := nESubR b x nHole). exact Hcd.
Qed.

Instance Es_nplug_Proper (C : nctx) : Proper (Es ==> Es) (nplug C).
Proof. intros a b Hab. apply Es_ctx. exact Hab. Qed.

Instance Es_nfv_Proper (z : atom) : Proper (Es ==> iff) (fun t => In z (nfv t)).
Proof. intros a b Hab. apply (Es_fv a b Hab z). Qed.

(* The reduction relation modulo Es, as in the paper:
   t ->sub t' iff there are s, s' with t =Es s ->sm s' =Es t'. *)
Definition subred (t t' : ntrm) : Prop :=
  exists s, exists s', Es t s /\ nred s s' /\ Es s' t'.

Lemma subred_intro : forall t s s' t',
    Es t s -> nred s s' -> Es s' t' -> subred t t'.
Proof. intros. unfold subred. exists s, s'. split; [| split]; assumption. Qed.

Lemma subred_nred : forall t u, nred t u -> subred t u.
Proof.
  intros t u H. apply subred_intro with (s := t) (s' := u).
  - apply Es_refl.
  - exact H.
  - apply Es_refl.
Qed.

Lemma subred_Es_l : forall t s u, Es t s -> subred s u -> subred t u.
Proof.
  intros t s u Ht [a [b [Ha [Hn Hb]]]].
  apply subred_intro with (s := a) (s' := b).
  - apply Es_trans with (u := s); assumption.
  - exact Hn.
  - exact Hb.
Qed.

Lemma subred_Es_r : forall t u v, subred t u -> Es u v -> subred t v.
Proof.
  intros t u v [a [b [Ha [Hn Hb]]]] Huv.
  apply subred_intro with (s := a) (s' := b).
  - exact Ha.
  - exact Hn.
  - apply Es_trans with (u := u); assumption.
Qed.

Lemma subred_Es_lr : forall t s s' t',
    Es t s -> subred s s' -> Es s' t' -> subred t t'.
Proof.
  intros t s s' t' Hts Hss' Hs't'.
  apply subred_Es_r with (u := s').
  - apply subred_Es_l with (s := s); assumption.
  - exact Hs't'.
Qed.

Lemma subred_context : forall C t t', subred t t' -> subred (nplug C t) (nplug C t').
Proof.
  intros C t t' [a [b [Ha [Hn Hb]]]].
  apply subred_intro with (s := nplug C a) (s' := nplug C b).
  - apply Es_ctx. exact Ha.
  - apply nred_ctx. exact Hn.
  - apply Es_ctx. exact Hb.
Qed.

Lemma subred_context_rule : forall C t t', nred t t' -> subred (nplug C t) (nplug C t').
Proof. intros. apply subred_context. apply subred_nred. exact H. Qed.

Lemma subred_of_Es_nred_Es : forall t s s' t',
    Es t s -> nred s s' -> Es s' t' -> subred t t'.
Proof. intros. apply subred_intro with (s := s) (s' := s'); assumption. Qed.

(* The rules are stable modulo Es: rewriting the redex or the reduct by Es
   gives a valid subred step. *)
Lemma nred_stable_source : forall t s u, Es t s -> nred s u -> subred t u.
Proof. intros. apply subred_intro with (s := s) (s' := u); [exact H | exact H0 | apply Es_refl]. Qed.

Lemma nred_stable_target : forall t u v, nred t u -> Es u v -> subred t v.
Proof. intros. apply subred_intro with (s := t) (s' := u); [apply Es_refl | exact H | exact H0]. Qed.

Print Assumptions Es_Equivalence.
Print Assumptions Es_NApp_Proper.
Print Assumptions Es_NLam_Proper.
Print Assumptions Es_NESub_Proper.
Print Assumptions Es_nplug_Proper.
Print Assumptions Es_nfv_Proper.
Print Assumptions subred_nred.
Print Assumptions subred_Es_l.
Print Assumptions subred_Es_r.
Print Assumptions subred_context.
Print Assumptions nred_stable_source.
Print Assumptions nred_stable_target.

Inductive StarN (R : ntrm -> ntrm -> Prop) : ntrm -> ntrm -> Prop :=
| starN_refl : forall t, StarN R t t
| starN_step : forall t u v, R t u -> StarN R u v -> StarN R t v.

Inductive PlusN (R : ntrm -> ntrm -> Prop) : ntrm -> ntrm -> Prop :=
| plusN1 : forall t u, R t u -> PlusN R t u
| plusNS : forall t u v, R t u -> PlusN R u v -> PlusN R t v.

Lemma StarN_trans : forall R a b c, StarN R a b -> StarN R b c -> StarN R a c.
Proof.
  intros R a b c H. induction H; intros Hbc.
  - exact Hbc.
  - apply starN_step with (u := u). exact H. apply IHStarN. exact Hbc.
Qed.

Lemma StarN_one_trans : forall R a b c, R a b -> StarN R b c -> StarN R a c.
Proof. intros. apply starN_step with (u := b); assumption. Qed.

Lemma PlusN_to_StarN : forall R t u, PlusN R t u -> StarN R t u.
Proof.
  intros R t u H. induction H.
  - apply starN_step with (u := u); [exact H | apply starN_refl].
  - apply starN_step with (u := u); [exact H | exact IHPlusN].
Qed.

Lemma StarN_subred_context : forall C t t',
    StarN subred t t' -> StarN subred (nplug C t) (nplug C t').
Proof.
  intros C t t' H. induction H.
  - apply starN_refl.
  - apply starN_step with (u := nplug C u).
    + apply subred_context. exact H.
    + exact IHStarN.
Qed.

Print Assumptions StarN_trans.
Print Assumptions StarN_one_trans.
Print Assumptions PlusN_to_StarN.
Print Assumptions StarN_subred_context.