LAFwE.v

Set Implicit Arguments.
Unset Strict Implicit.
Generalizable All Variables.
Typeclasses eauto := 1.

Require Import ssreflect List Basic LAF.

Definition comp {A B C} (g:B -> C) (f:A -> B) x := g(f x).

Section LAFwE.
  (*************************)
  (* Quantifying Structure *)
  (*************************)

  Definition QSwE2QS_base So Te SoR : QuantifyingStructures :=
    {|
      Sorts := So;
      QWorld := Type;
      Terms := Te;
      SoContexts qLab := qLab -> So;
      SortingRel := SoR
    |}
  .

  Class QuantifyingStructureswE {So Te SoR}
    := 
      {
        asQS: SClass (@QSwE2QS_base So Te SoR);

        asT (qLab: QWorld (get asQS)): qLab -> Terms qLab;

        lift2Terms qLab qLab' 
        : (qLab -> qLab') -> Terms (q:= get asQS) qLab -> Terms (q:= get asQS) qLab';

        lift2Terms_asT qLab qLab' (f:qLab -> qLab')
        : forall xq:qLab, lift2Terms f (asT xq) = asT (f xq);

        lift2Terms_comp qLab0 qLab1 qLab2
                        (f1:qLab0 -> qLab1)
                        (f2:qLab1 -> qLab2)
                        (f3:qLab0 -> qLab2)
        : (forall xq:qLab0, f3 xq = f2(f1 xq))
          -> (forall t:Terms (q:= get asQS) qLab0, lift2Terms f3 t = lift2Terms f2(lift2Terms f1 t));

        qLabSorting qLab : 
          forall Sigma (xq:qLab) s, SortingRel Sigma (asT xq) s <-> s = Sigma xq;

        renSorting qLab qLab' :
          forall (pi:qLab -> qLab') Sigma Sigma' r s, 
            (forall xq, Sigma(pi xq) = Sigma' xq)
            -> SortingRel (q:=get asQS) Sigma' r s
            -> SortingRel (q:=get asQS) Sigma (lift2Terms pi r) s;

        wextendsE : DecStruct -> World (get asQS) -> World (get asQS)
      }.

  Canonical QSwE2QS `(QuantifyingStructureswE) := @QSwE2QS_base So Te SoR.

  (* Renaming in term lists and instantiated things *)

  Fixpoint renTList `{QuantifyingStructureswE}
           qLab qLab' l (pi:qLab -> qLab') (tl: TList qLab l) : TList qLab' l
  := match tl with
        | TermNil => TermNil _ _
        | TermCons so r l' tl' => TermCons so (lift2Terms pi r) (renTList pi tl')
    end.

  Lemma renTList_comp `{QuantifyingStructureswE} qLab0 qLab1 qLab2
        (f1:qLab0 -> qLab1)
        (f2:qLab1 -> qLab2)
        (f3:qLab0 -> qLab2)
        ls
  : (forall xq:qLab0, f3 xq = f2(f1 xq))
    -> (forall tl:TList qLab0 ls, renTList f3 tl = renTList f2(renTList f1 tl)).
  Proof.
    move => H0.
    elim => //.
    move => s head l tail IH /=.
    rewrite IH (lift2Terms_comp (qLab1 := qLab1) (f1 := f1) (f2 := f2) _ head) => //.
  Qed.

  Definition renInst `{QuantifyingStructureswE}
             qLab qLab' (pi:qLab -> qLab')
             {A} (Alr: Inst A qLab): Inst A qLab'
    := [getA Alr,renTList pi (getTerms Alr)].

  Lemma renInst_comp `{QuantifyingStructureswE} qLab0 qLab1 qLab2
        (f1:qLab0 -> qLab1)
        (f2:qLab1 -> qLab2)
        (f3:qLab0 -> qLab2)
        A
  : (forall xq:qLab0, f3 xq = f2(f1 xq))
    -> (forall Alr: Inst A qLab0, renInst f3 Alr = renInst f2(renInst f1 Alr)).
  Proof.
    move => H0.
    elim => //.
    move => x p /=.
    rewrite /renInst /= (renTList_comp (qLab1 := qLab1) (f1 := f1) (f2 := f2)) => //.
  Qed.

  (* Enriching Quantifying structures with types (instantiated atoms
  and molecules), now with eigenvariables *)

  Definition QSTwE2QST_base `(QSV:QuantifyingStructureswE) AtomV MoleculeV is_eqV: QSTypes :=
    {|
      QS := QSwE2QS _;
      Atom := AtomV;
      Molecule := MoleculeV;
      is_eq := is_eqV
    |}
  .

  Class QSTypeswE `(QSwE : QuantifyingStructureswE) AtomV MoleculeV is_eqV
    := 
      {
        Extren {w:World (get asQS)} st: (w.(QLab):Type) -> ((wextendsE st w).(QLab):Type);
        Extst  {w:World (get asQS)} st: @Dec (wextendsE st w).(QLab) unit unit st;
        asQSwE := QSwE;
        asQST := QSTwE2QST_base (QSV:=QSwE) (AtomV:=AtomV) MoleculeV is_eqV;
        is_eq_ren {qLab qLab'} 
        : forall IA IA' : Inst (Atom (q:=asQST)) qLab,
            is_eq IA IA'
            -> forall pi:qLab -> qLab', is_eq (q:=asQST) (renInst pi IA) (renInst pi IA')
      }.
  
  Coercion asQSwE: QSTypeswE >-> QuantifyingStructureswE.

  Canonical QSTwE2QST `(QSTypeswE)
    := QSTwE2QST_base (QSV:=QSwE) (AtomV:=AtomV) MoleculeV is_eqV.

  (* Stuff about generic contexts *)

  Definition ContextswE `{QuantifyingStructureswE} A B C
    := Contexts wextendsE A B C (fun qLab => (qLab:Type) -> C).

  Definition renProp
             `{QSTypeswE} 
             `(Cont: ContextswE A B C)
    := forall w st (Gamma:Cont w) Delta xq, 
        readE (extends Delta Gamma)(Extren st xq) = readE Gamma xq.

  Definition stProp
             `{QSTypeswE} 
             `(Cont: ContextswE A B C)
    := forall w st (Gamma:Cont w) Delta,
        Declift (fun s xq => s = readE (extends Delta Gamma) xq)
                (fun _ _ => True)
                (fun _ _ => True)
                Delta (Extst st).

  Definition Contlift `{QSTypeswE}{E F A B C D:Type}
             (RelQ: E -> F -> Prop)
             (RelP: A -> C -> Prop)
             (RelN: B -> D -> Prop)
             {Context1 : ContextswE A B E}
             {Context2 : ContextswE C D F}
             {w} 
  : Context1 w -> Context2 w -> Prop
    := fun Gamma rho =>
        (forall xq, RelQ (readE Gamma xq) (readE rho xq))
        /\ (forall xp, RelP (readp Gamma xp) (readp rho xp))
        /\ (forall xn, RelN (readn Gamma xn) (readn rho xn))
  .

  Definition ContMap `{QSTypeswE}{E F A B C D:Type}
             (fQ: E -> F)
             (fP: A -> C)
             (fN: B -> D)
             {Context1 : ContextswE A B E}
             {Context2 : ContextswE C D F}
             {w} 
  : Context1 w -> Context2 w -> Prop
    := Contlift (fun c c' => c' = fQ c) (fun c c' => c' = fP c) (fun c c' => c' = fN c).

  (* Now we define typing contexts in the sense of LAF with eigenvariables *)

  Context `(QSTV: QSTypeswE).

  Class TContextswE :=
    {
      TCstruct (qLab: QWorld (QSTwE2QST QSTV))
      : ContextswE (Inst Atom qLab) 
                   (Inst Molecule qLab) 
                   (Sorts (QSwE2QS QSTV));

      TCmap (qLab qLab': QWorld (QSTwE2QST QSTV)) w :
        forall (f1: Inst Atom qLab -> Inst Atom qLab')
          (f2: Inst Molecule qLab -> Inst Molecule qLab'),
          ((TCstruct qLab).(Csupport) w)
          -> ((TCstruct qLab').(Csupport) w);

      TCmapProp qLab qLab' w
                (f1: Inst Atom qLab -> Inst Atom qLab')
                (f2: Inst Molecule qLab -> Inst Molecule qLab')
                (Gamma: TCstruct qLab w)
      : ContMap (fun i => i) f1 f2 Gamma (TCmap f1 f2 Gamma)
    }
  .

  Coercion TCstruct: TContextswE >-> Funclass.
  
  Definition InstTypingDec {qLab:QWorld _} {st ls}
             (qn : @Dec qLab unit unit st)
             (lq: TList qLab ls)
             (Delta:TypingDec st ls)
  : @Dec (Sorts (QSwE2QS QSTV)) (Inst Atom qLab) (Inst Molecule qLab) st.
  Proof.
    induction Delta.
    exact (leafP([a,lq])).
    exact (leafN([m,lq])).
    exact (dummy).
    inversion qn.
    exact (node (IHDelta1 X lq) (IHDelta2 X0 lq)).
    inversion qn.
    exact (qnode so (IHDelta X0 (TermCons so (asT X) lq))).
  Defined.

  Coercion TContextwE2TContext `(TCV: TContextswE) :=
    {|
      TCsupport w := TCV w.(QLab) w;
      Treadp w := readp (c := TCV w.(QLab)) (w:=w);
      Treadn w := readn (c := TCV w.(QLab)) (w:=w);
      TreadE w := readE (c := TCV w.(QLab)) (w:=w);
      Textends w st Deltal Gamma :=
        extends (st:=st) (c:=TCV (wextendsE st w).(QLab))
                (InstTypingDec (qLab := (wextendsE st w).(QLab)) 
                               (Extst st) 
                               (renTList (Extren st) (getTerms Deltal)) 
                               (getA Deltal))
                (TCmap (renInst (Extren st)) (renInst (Extren st)) Gamma)
    |}
  .

End LAFwE.

Definition LAFwE2LAF_base
          `{QSTV:QSTypeswE}
          (TCV: TContextswE _) 
          {PatternsV PatDecV PatternsTypedV} :=
  {|
    QST := QSTwE2QST QSTV;
    wextends := wextendsE;
    TContext := TCV;
    Patterns := PatternsV;
    PatDec   := PatDecV;
    PatternsTyped := PatternsTypedV
  |}.

Class LAFswE `{QSTV:QSTypeswE} {PatternsV PatDecV PatternsTypedV} :=
  {
    asQSTwE := QSTV;
    TCV : TContextswE _;
    asLAF := LAFwE2LAF_base (QSTV:=QSTV)
                      TCV
                      (PatternsV:=PatternsV)
                      (PatDecV:=PatDecV)
                      (PatternsTypedV:=PatternsTypedV)
  }.

Coercion asQSTwE: LAFswE >-> QSTypeswE.

Canonical LAFwE2LAF `(LAFswE)
  := LAFwE2LAF_base (QSTV:=QSTV) TCV
                   (PatternsV:=PatternsV)
                   (PatDecV:=PatDecV)
                   (PatternsTypedV:=PatternsTypedV)
.


Definition GenericCorr `{QSTypeswE}{E F A B C D:Type} 
           (RelQ: E -> F -> Prop)
           (RelP: A -> C -> Prop)
           (RelN: B -> D -> Prop)
           {Context1 : ContextswE A B E}
           {Context2 : ContextswE C D F}
:= forall w st (Gamma:Context1 w) (rho:Context2 w) v Delta,
    Declift RelQ RelP RelN (st:=st) Delta v
    -> Contlift RelQ RelP RelN Gamma rho 
    -> Contlift RelQ RelP RelN (extends Delta Gamma) (extends v rho).