RSC.lib

Require Import Lt Le List Compare_dec Plus Minus EqNat Bool Omega Program.Equality.
From Autosubst Require Export Autosubst.
Require Export RSC.Decidable.

(* basic definitions *)
Definition rel_func {X Y} (R : X -> Y -> Prop) := forall x y y', R x y -> R x y' -> y = y'.
Definition rel_inj {X Y} (R : X -> Y -> Prop) := forall x x' y, R x y -> R x' y -> x = x'.

(* we construct a an instance of class Monad for Coq's option type *)
Class Functor (F : Type -> Type) := {fmap {X Y} : (X -> Y) -> F X -> F Y}.
Infix "<$>" := fmap (left associativity, at level 11).

Class Monad (m : Type -> Type) :=
  {
    bind {X Y} : m X -> (X -> m Y) -> m Y;
    ret {X} : X -> m X
  }.

Notation "'do' x <- a ; s" := (bind a (fun x => s)) (right associativity, at level 100).

Notation "'GET' x <- a ; P" := (match a with Some x => P | _ => False end) (right associativity, at level 100).

Instance Functor_Monad {m} {_ : Monad m} : Functor m :=
  { fmap X Y f a := do a' <- a; ret(f a') }.

Instance : Monad option :=
  {
    bind X Y a f := match a with None => None | Some a' => f a' end;
    ret X := Some
  }.

(* some notations *)
Notation "(-1)" := (0 .: id).

(* ltac tools *)
Tactic Notation "getH" open_constr(T) := match goal with [H : context[T] |- _] => exact H end.

Notation "$$( T )" := ltac:(getH T) (only parsing).
Notation "$?" := ltac:(eauto; econstructor; try econstructor; now eauto) (only parsing).

Ltac clean_goal := repeat
  match goal with
      [H : ?s = ?s |- _] => clear H
    | [H : ?T |- _] => match T with _ /\ _ => idtac | (_,_) => idtac end; destruct H
  end.

Ltac autodestr := repeat (clean_goal; try subst; simpl; match goal with [|- context[match ?s with _ => _ end]] =>
                                                            try match s with context[match _ with _ => _ end] => fail 2 end;
                                                                         destruct s eqn:? end); try subst; simpl; trivial.

(* sensible inversion tactic *)
Ltac inv H := inversion H; clear H; subst.

(* TODO: check if the Monad instance for Option, $(T), and autodestr are really need for this section *)
Section Lookup.

  Context {term : Type}.
  Context {Ids_term : Ids term} {Rename_term : Rename term}
          {Subst_term : Subst term} {SubstLemmas_term : SubstLemmas term}.

  (* standard context lookup *)
  Inductive atn: list term -> var -> term -> Prop :=
  | Atn0 Delta A : atn (A :: Delta) 0 A
  | AtnS Delta x A B :
      atn Delta x B -> atn (A :: Delta) (S x) B.

  Fixpoint get Gamma {struct Gamma} : var -> option term :=
    match Gamma with
    | nil => (fun n => None)
    | s :: Gamma => Some s .: get Gamma
    end.

  Lemma get_atn Gamma n s : get Gamma n = Some s -> atn Gamma n s.
  Proof.
    revert n s. induction Gamma; intros n s E.
    - inversion E.
    - destruct n as [|n]; simpl in E.
      + inversion E; subst. constructor.
      + constructor; auto.
  Qed.

  Lemma atn_get Gamma n s : atn Gamma n s -> get Gamma n = Some s.
  Proof. induction 1; intros; subst; simpl; now autorew. Qed.

  Lemma mmap_atn {f : term -> term} {Gamma x A'} :
    atn (mmap f Gamma) x A' -> exists A, A' = (f A) /\ atn Gamma x A.
  Proof.
    intros H. depind H.
    - destruct Gamma; ainv. eexists. eauto using atn.
    - destruct Gamma; try now ainv.
      simpl in x.
      inversion x.
      destruct (IHatn _ _ _ $$(Gamma)) as [ B' [H_eq H_atn]].
      exists B'. eauto using atn.
  Qed.

  Lemma atn_mmap {f : term -> term} {Gamma x A A'} :
    atn Gamma x A -> A' = (f A) -> atn (mmap f Gamma) x A'.
  Proof. induction 1; intros; subst; constructor; eauto. Qed.

  Lemma mmap_get {f : term -> term} {Gamma x A'} :
    get (mmap f Gamma) x = Some A' -> exists A, A' = (f A) /\ get Gamma x = Some A.
  Proof.
    intros H. apply get_atn in H. destruct (mmap_atn H) as [A [EA H']].
    exists A; eauto using atn_get.
  Qed.

  Lemma get_mmap {f : term -> term} {Gamma x A A'} :
    get Gamma x = Some A -> A' = (f A) -> get (mmap f Gamma) x = Some A'.
  Proof. intros. apply atn_get. apply get_atn in H. eapply atn_mmap; eauto. Qed.

  Lemma mmap_get_None {f : term -> term} {Gamma x} :
    get (mmap f Gamma) x = None -> get Gamma x = None.
  Proof.
    intros H. case_eq (get Gamma x); trivial. intros t Et. exfalso.
    eapply @get_mmap with (f:=f) in Et; eauto. congruence.
  Qed.

  Lemma get_mmap_None {f : term -> term} {Gamma x} :
    get Gamma x = None -> get (mmap f Gamma) x = None.
  Proof.
    intros H. case_eq (get (mmap f Gamma) x); trivial. intros t Et. exfalso.
    destruct (mmap_get Et) as [s [_ H']]. congruence.
  Qed.

  (* dependent context lookup *)
  Inductive atnd: list term -> var -> term -> Prop :=
  | Atnd0 Delta A A' :
      A' = A.[ren(+1)] -> atnd (A :: Delta) 0 A'
  | AtndS Delta x A B B' :
      atnd Delta x B -> B' = B.[ren(+1)] -> atnd (A :: Delta) (S x) B'.

  Fixpoint getD (Gamma : list term) n : option term :=
    match Gamma with
      | nil => fun n => None
      | s :: Gamma => Some s.[ren(+1)] .: getD Gamma >>> fmap(subst(ren(+1)))
    end n.
  Arguments getD !Gamma/ n.

  Lemma getD_atnd Gamma n s : getD Gamma n = Some s -> atnd Gamma n s.
  Proof.
    revert n s. induction Gamma; intros n s E.
    - inversion E.
    - destruct n as [|n].
      + simpl in E. inversion E; subst. now constructor.
      + simpl in E. case_eq (getD Gamma n); [intros t E'|intros E']; rewrite E' in E; inversion E; subst.
        econstructor; eauto.
  Qed.

  Lemma atnd_getD Gamma n s : atnd Gamma n s -> getD Gamma n = Some s.
  Proof. induction 1; intros; subst; simpl; now autorew. Qed.

  (* atnd is a functional relation *)
  Lemma atnd_func Gamma : rel_func (atnd Gamma).
  Proof. intros x A A' H; revert A'. induction H; intros C J; ainv. now rewrite (IHatnd _ H3). Qed.

  (* Connecting the two notions *)
  Lemma getD_get Gamma n : getD Gamma n = subst (ren(+S n)) <$> (get Gamma n).
  Proof.
    revert Gamma; induction n; intros; destruct Gamma; simpl; autorew; trivial.
    asimpl. autodestr. autosubst.
  Qed.

  Lemma getD_cons (s : term) (Gamma : list term) :
    getD (s :: Gamma) = (Some s.[ren (+1)]) .: getD Gamma..[ren (+1)].
  Proof.
    f_ext. intros [|n]; trivial. rewrite getD_get.
    replace ((Some s.[ren (+1)] .: getD Gamma..[ren (+1)]) (S n)) with (getD Gamma..[ren (+1)] n) by reflexivity.
    repeat rewrite getD_get. asimpl.
    case_eq (get Gamma n).
    - intros t Et.
      assert (E: get Gamma..[ren (+1)] n = Some t.[ren (+1)]) by (eapply get_mmap; eauto).
      rewrite E; autosubst.
    - intros E. rewrite get_mmap_None; trivial.
  Qed.

End Lookup.

Ltac atom_ren :=
  (repeat
    match goal with
      | [H : ?T = ?S.[ren ?xi] |- _] => (destruct S; simpl in H; try discriminate H);[idtac]; try match goal with [H : T = T |- _] => clear H end
      | [H : ?S.[ren ?xi] = ?T |- _] => (destruct S; simpl in H; try discriminate H);[idtac]; try match goal with [H : T = T |- _] => clear H
                                                                                               end
    end); ainv.

Lemma decide_refl {X Y} (a : X) (_ : Dec (a = a)) (s t : Y) : (if decide (a = a) then s else t) = s.
Proof. decide (a = a); congruence. Qed.

Ltac simpG := simpl in *; repeat match goal with
                                | [H : context[if decide (?s = ?s) then _ else _] |- _] => rewrite decide_refl in H
                                end.

Ltac ca := simpG; repeat match goal with
                          | [|- context[match ?s with _ => _ end]] => ( assert True as _; (destruct s eqn:?; simpG; try contradiction; try congruence; eauto)); [trivial | fail..]
                                                                                                                                                                    | [H : context[match ?s with _ => _ end] |- _] => ( assert True as _; (destruct s eqn:?; simpG; try contradiction; try congruence; eauto)); [trivial | fail..]
                          end.

Ltac subst' := repeat progress match goal with [x : _ |- _] => subst x end.
Ltac clear_rec := first[subst | match goal with [H : _ = _ |- _] => clear H; subst end].

Ltac aspec := repeat match goal with
                      | [H : _ |- _] => first[ specialize (H _ _ _ $?) | specialize (H _ _ $?) | specialize (H $?) | specialize (H _ $?) ] end.

Definition sum2bool {A B} (x : A + B) := if x then true else false.

Coercion sum2bool : sum >-> bool.

Definition comb {X Y} (bits : X -> bool) f g x : Y := if bits x then f x else g x.
Arguments comb {X Y} bits f g x/.

Lemma comb_cons {X} bits (sigma tau : var -> X) : comb bits sigma tau = (if bits 0 then sigma 0 else tau 0) .: comb ((+1) >>> bits) ((+1) >>> sigma) ((+1) >>> tau).
Proof. f_ext. intros [|]; reflexivity. Qed.

Lemma comb_comp {A B C} (bits : A -> bool) sigma tau (f : B -> C) : comb bits sigma tau >>> f = comb bits (sigma >>> f) (tau >>> f).
Proof. f_ext; intros. simpl. destruct (bits x); reflexivity. Qed.

Lemma upren_comb bits xi zeta b : upren (comb bits xi zeta) = comb (b .: bits) (upren xi) (upren zeta).
Proof. setoid_rewrite comb_cons at 2. destruct b; asimpl; unfold upren; now rewrite comb_comp. Qed.
(* Q-JK: before now: both S and (+1) appear in goal *)

(* Lemma upren_injective xi : injective xi -> injective (upren xi). *)
(* Proof. intros I |x |y E; asimpl in *; eauto; discriminate E. Qed. *)

(* Generic context renamings *)

Section ContextRenamings.

  Context {term : Type}.
  Context {Ids_term : Ids term} {Rename_term : Rename term}
          {Subst_term : Subst term} {SubstLemmas_term : SubstLemmas term}.

  Definition cr xi Gamma Delta := forall n t, atnd Gamma n t -> atnd Delta (xi n) t.[ren xi].

  Lemma cr_up t xi Gamma Delta : cr xi Gamma Delta -> cr (upren xi) (t :: Gamma) (t.[ren xi] :: Delta).
  Proof. intros c [|] s l; inversion l; subst; econstructor; eauto; autosubst. Qed.

  Lemma cr_shift Gamma t : cr (+1) Gamma (t :: Gamma).
  Proof. intros n s l. asimpl. econstructor; eauto. Qed.

End ContextRenamings.

Section CtxBoolFun.

  Context {term : Type}.
  Context {Ids_term : Ids term} {Rename_term : Rename term}.

  Definition bfr (xi : var -> var) delta gamma := forall n, gamma n = true -> delta (xi n) = true.

  Lemma bfr_up b xi delta gamma : bfr xi delta gamma -> bfr (upren xi) (b .: delta) (b .: gamma).
  Proof. intros H [|n] e; asimpl; eauto. Qed.

  Lemma bfr_shift b gamma : bfr (+1) (b .: gamma) gamma.
  Proof. intros n e. trivial. Qed.

  Lemma bfr_ushift gamma : bfr (-1) gamma (false .: gamma).
  Proof. intros [|n]; asimpl; trivial. discriminate. Qed.

End CtxBoolFun.

Section Coincidence.

  Context {term : Type}.
  Context {Ids_term : Ids term} {Rename_term : Rename term}
          {Subst_term : Subst term} {SubstLemmas_term : SubstLemmas term}.

  Definition subst_coinc (gamma : var -> bool) (sigma tau : var -> term) := forall n, gamma n = true -> sigma n = tau n.

  Lemma subst_coinc_id gamma sigma : subst_coinc gamma sigma sigma.
  Proof. now intros n. Qed.

  Lemma subst_coinc_up b gamma sigma tau : subst_coinc gamma sigma tau -> subst_coinc (b .: gamma) (up sigma) (up tau).
  Proof. intros H [|n] A; asimpl in *; trivial. now rewrite H. Qed.

  (* Lemma ren_coinc_hd_f b gamma xi zeta : b = false -> subst_coinc gamma (ren xi) tau -> subst_coinc (b .: gamma) (ren (x .: xi)) (ren (z .: zeta)). *)
  (* Proof. intros E H |n A; asimpl in *; try congruence. now apply H. Qed. *)

  Lemma subst_coinc_hd_f b gamma sigma tau : b = false -> subst_coinc gamma ((+1) >>> sigma) ((+1) >>> tau) -> subst_coinc (b .: gamma) sigma tau.
  Proof. intros E H [|n] A; asimpl in *; try congruence. now apply (H n). Qed.

End Coincidence.

Section CoincidenceHSubst.

  Context {type : Type}.
  Context {Ids_type : Ids type} {Rename_type : Rename type}
          {Subst_type : Subst type} {SubstLemmas_type : SubstLemmas type}.

  Context {term : Type}.
  Context {Ids_term : Ids term} {Rename_term : Rename term}
          {Subst_term : Subst term} {SubstLemmas_term : SubstLemmas term}
          {HSubst_term : HSubst type term} {HSubstLemmas_term : HSubstLemmas type term}.

  Lemma subst_coinc_hcomp gamma sigma tau rho : subst_coinc gamma sigma tau -> subst_coinc gamma (sigma >>| rho) (tau >>| rho).
  Proof. intros H n E. asimpl. f_equal. eauto. Qed.

End CoincidenceHSubst.