Accompanying code for https://ptival.github.io/deep-dive-meta-theory-carte-3 (NOTE: there should be a "Download ZIP" button in the top-right corner)

.gitignore

*.aux
*.glob
*.vo
*.vok
*.vos
.envrc
.Makefile.coq.d
Makefile.coq
Makefile.coq.conf

_CoqProject

-arg -impredicative-set

-Q . MTC

Hacks.v

### Theory
Algebra.v
Functor.v
IndexedAlgebra.v
IndexedFunctor.v
IndexedSubFunctor.v
IndexedSum1.v
SubFunctor.v
Sum1.v

### Extensible functions and relations
Eval.v
Soundness.v
TypeEquality.v
TypeOf.v
WellTypedValue.v
WellTypedValueProjection.v

### Types
BooleanType.v
NaturalType.v

### Features
Boolean.v
Natural.v
Stuck.v

### Demo
Demo.v

Algebra.v

From Coq Require Import
     ssreflect
.

From MTC Require Import
     Functor
     SubFunctor
     Sum1
.

Local Open Scope SubFunctor.

(** A regular [Algebra]. *)
Definition Algebra (F : Set -> Set) (A : Set) : Set :=
  F A -> A.

(**
[MendlerAlgebra]s give us control over when recursion happens.
 *)
Definition MendlerAlgebra (F : Set -> Set) (A : Set) : Set :=
  forall (R : Set), (R -> A) -> F R -> A.

(**
[Fix] turns a functor [F] into its fixed point [Set], being the set of all folds
of its [MendlerAlgebra]s.
 *)
Definition Fix (F : Set -> Set) : Set :=
  forall (A : Set), MendlerAlgebra F A -> A.

(**
[ProgramAlgebra] is simply a type class wrapper around [MendlerAlgebra]s, with
an extra [Tag] so as to help type class resolution pick the correct instances.
 *)
Class ProgramAlgebra (Tag : Set) F A :=
  {
    programAlgebra : MendlerAlgebra F A;
  }.

Global Instance ProgramAlgebra__Sum1
       (Tag : Set) (F G : Set -> Set)
       (A : Set)
       `{ProgramAlgebra Tag F A}
       `{ProgramAlgebra Tag G A}
  : ProgramAlgebra Tag (F + G)%Sum1 A
  :=
    {|
      programAlgebra :=
        fun _ rec s =>
          match s with
          | inl1 l => programAlgebra _ rec l
          | inr1 r => programAlgebra _ rec r
          end
    |}.

(**
A [MendlerAlgebra] can be used to fold a [Fix E] simply by applying the algebra.
 *)
Definition mendlerFold
           {E A} (alg : MendlerAlgebra E A)
  : Fix E -> A
  := fun e => e A alg.

(**
A simple [Algebra] can also be used to fold a [Fix E].
 *)
Definition fold
           {E A} `{Functor E} (alg : Algebra E A)
  : Fix E -> A
  := mendlerFold (fun r rec fa => alg (fmap rec fa)).

(**
[wrapF] lets us wrap an unwrapped [E (Fix E)] into a [Fix E].  Eventually, we'll
want a more general wrapping from an [F (Fix E)] into a [Fix E], which will be
possible when [E supports F].
 *)
Definition wrapF
           {E} (unwrapped : E (Fix E))
  : Fix E
  := fun A f => f _ (mendlerFold f) unwrapped.

(**
Conversely, [unwrapF] unfolds a [Fix E] into an [E (Fix E)].  Again, we will
eventually want to "cast" down into a feature [F (Fix E)], though this will
not always work: if the wrapped expression was a [G (Fix E)] for [F <> G],
the casting down will fail.
 *)
Definition unwrapF
           {E} `{Functor E}
  : Fix E -> E (Fix E)
  := fold (fmap wrapF).

(**
[projectF] lets us inspect a wrapped expression, and ask the question "is it an
expression of this given feature?".  If it is, it returns [Some f] where [f] has
type [F (Fix E)] for the feature [F] we are interested about.  If it is not, it
returns [None], indicating that the outermost constructor must belong to a
different feature.
 *)
Definition projectF
           {E F}
           `{Functor E} `{Functor F}
           `{E supports F}
           (e : Fix E)
  : option (F (Fix E))
  := project (unwrapF e).

Definition injectF
           {E F}
           `{Functor E} `{Functor F}
           `{E supports F}
           (f : F (Fix E))
  : Fix E
  := wrapF (inject f).

(* Lemma fold_wrapF *)
(*       {F} `{Functor F} *)
(*       (e : Fix F) *)
(*   : fold wrapF e = e. *)
(* Admitted. (* similar lemma to be proven in another blog post *) *)

Lemma unwrapF_wrapF
   {E} `{Functor E}
  : forall (e : E (Fix E)),
    unwrapF (wrapF e) = e.
Admitted. (* similar lemma to be proven in another blog post *)

Lemma wrapF_unwrapF
      {E} `{Functor E}
  : forall (e : Fix E),
    wrapF (unwrapF e) = e.
Admitted. (* similar lemma to be proven in another blog post *)

Lemma wrapF_inversion
      {E} `{Functor E}
  : forall (e e' : E (Fix E)),
      wrapF e = wrapF e' ->
      e = e'.
Proof.
  move => e e' / (f_equal unwrapF).
  rewrite ! unwrapF_wrapF.
  rewrite //.
Qed.

(* Class WellFormedProgramAlgebra *)
(*       {Tag F A} *)
(*       `{Functor F} *)
(*       `(ProgramAlgebra Tag F A) *)
(*   := *)
(*     { *)
(*       wellFormedProgramAlgebra *)
(*       : forall {A B : Set} (f : A -> B) rec (fa : F A), *)
(*         programAlgebra B rec (fmap f fa) = *)
(*         programAlgebra A (fun fa => rec (f fa)) fa *)
(*     }. *)

(** *)
(* NOTE: We have to specify [E := E] here, otherwise [inject] will pick *)
(* [SubFunctor__Refl] and not actually inject in [E], turning the statement into a *)
(* reflexive tautology. *)
(*  *)
Class WellFormedCompoundProgramAlgebra
      Tag E F {A}
      `{Functor E} `{Functor F}
      `{E supports F}
      `{ProgramAlgebra Tag E A}
      `{ProgramAlgebra Tag F A}
  :=
    {
      wellFormedCompoundProgramAlgebra
      : forall T rec fa,
        programAlgebra T rec (inject (E := E) fa)
        =
        programAlgebra T rec fa;
    }.

Global Instance WellFormedCompoundProgramAlgebra__Refl
       {Tag F A}
       `{Functor F}
       `{ProgramAlgebra Tag F A}
  : WellFormedCompoundProgramAlgebra Tag F F.
Proof.
  constructor.
  move => rec fa.
  rewrite /inject /SubFunctor__Refl => //.
Qed.

Global Instance
       WellFormedCompoundProgramAlgebra__Left
       {Tag F G H A}
       `{Functor F} `{Functor G} `{Functor H}
       `{! ProgramAlgebra Tag F A}
       `{! ProgramAlgebra Tag G A}
       `{! ProgramAlgebra Tag H A}
       `{! G supports F}
       `{! WellFormedCompoundProgramAlgebra Tag G F}
  : WellFormedCompoundProgramAlgebra Tag (G + H)%Sum1 F.
Proof.
  constructor.
  move => R rec f.
  rewrite /inject /SubFunctor__Left /=.
  rewrite wellFormedCompoundProgramAlgebra => //.
Qed.

Global Instance
       WellFormedCompoundProgramAlgebra__Right
       {Tag F G H A}
       `{Functor F} `{Functor G} `{Functor H}
       `{! ProgramAlgebra Tag F A}
       `{! ProgramAlgebra Tag G A}
       `{! ProgramAlgebra Tag H A}
       `{! H supports F}
       `{! WellFormedCompoundProgramAlgebra Tag H F}
  : WellFormedCompoundProgramAlgebra Tag (G + H)%Sum1 F.
Proof.
  constructor.
  move => rec f.
  rewrite /inject /SubFunctor__Right => fa /=.
  rewrite wellFormedCompoundProgramAlgebra //.
Qed.

Theorem projectF_injectF
        {E F}
        `{Functor E} `{Functor F}
        `{E supports F}
        {e : Fix E}
        {f : F (Fix E)}
  : projectF e = Some f ->
    e = injectF (E := E) f.
Proof.
Admitted. (* similar lemma to be proven in another blog post *)

Class ProofAlgebra (Tag : Set) F A :=
  {
    proofAlgebra : Algebra F A;
  }.

Global Instance
       ProofAlgebra__Sum1
       {Tag} F G {A}
       `{Functor F} `{Functor G}
       {FAlg : ProofAlgebra Tag F A}
       {GAlg : ProofAlgebra Tag G A}
  : ProofAlgebra Tag (F + G)%Sum1 A
  :=
    {|
      proofAlgebra :=
        fun fg =>
          match fg with
          | inl1 f => proofAlgebra f
          | inr1 g => proofAlgebra g
          end
      ;
    |}.

Lemma Induction
      {Tag F} `{Functor F}
      {P : Fix F -> Prop}
      `{ProofAlgebra Tag F (sig P)}
  : forall (f : Fix F),
    P f.
Admitted. (* similar lemma to be proven in another blog post *)

Lemma discriminate_inject
      {F G H : Set -> Set}
      `{Functor F}
      `{Functor G}
      `{Functor H}
      `{H supports F}
      `{H supports G}
  : forall A (f : F A) (g : G A),
    inject (E := H) f <> inject (E := H) g.
Admitted. (* similar lemma to be proven in another blog post *)

Boolean.v

From Coq Require Import
     ssreflect
.

From MTC Require Import
     Algebra
     BooleanType
     Eval
     Functor
     Hacks
     IndexedAlgebra
     IndexedFunctor
     IndexedSubFunctor
     Soundness
     Stuck
     SubFunctor
     TypeEquality
     TypeOf
     WellTypedValue
     WellTypedValueProjection
.

Local Open Scope SubFunctor.

Inductive Boolean (E : Set) : Set :=
| MkBoolean (b : bool)
| IfThenElse (condition thenBranch elseBranch : E)
.
Arguments MkBoolean  {E}.
Arguments IfThenElse {E}.

Global Instance Functor__Boolean
  : Functor Boolean
  :=
    {|
      fmap :=
        fun _ _ f v =>
          match v with
          | MkBoolean b      => MkBoolean b
          | IfThenElse c t e => IfThenElse (f c) (f t) (f e)
          end
    |}.

Definition boolean
           {E} `{Functor E} `{E supports Boolean}
           (b : bool)
  : Fix E
  := injectF (MkBoolean b).

Definition ifThenElse
           {E} `{Functor E} `{E supports Boolean}
           (c t e : Fix E)
  : Fix E
  := injectF (IfThenElse c t e).

Definition isBoolean
           {E} `{Functor E} `{E supports Boolean}
  : Fix E -> option bool
  := fun v =>
       match projectF v with
       | Some (MkBoolean b) => Some b
       | _                  => None
       end.

Global Instance Eval__Boolean
       V `{Functor V}
       `{V supports Boolean}
       `{V supports Stuck}
  : ProgramAlgebra ForEval Boolean (EvalResult V)
  :=
    {|
      programAlgebra :=
        fun _ rec b =>
          match b with
          | MkBoolean b      => boolean b
          | IfThenElse c t e =>
            match isBoolean (rec c) with
            | Some b => if b then rec t else rec e
            | _      => stuck IfConditionNotBoolean
            end
          end
    |}.

Global Instance TypeOf__Boolean
       {T} `{Functor T} `{T supports BooleanType}
       {TypeEquality__T : ProgramAlgebra ForTypeEquality T (TypeEqualityResult T)}
  : ProgramAlgebra ForTypeOf Boolean (TypeOfResult T)
  :=
    {|
      programAlgebra :=
        fun _ rec v =>
          match v with
          | MkBoolean _ => Some booleanType
          | IfThenElse c t e =>
            match rec c with
            | Some tau__c =>
              if isBooleanType tau__c
              then
                match (rec t, rec e) with
                | (Some tau__t, Some tau__e) =>
                  if typeEquality tau__t tau__e
                  then Some tau__t
                  else None
                | _ => None
                end
              else None
            | None => None
            end
          end
      ;
    |}.

Inductive WellTypedValue__Boolean
          {T E}
          `{Functor T} `{Functor E}
          `{T supports BooleanType}
          `{E supports Boolean}
          (WTV : TypedExpr T E -> Prop)
  : TypedExpr T E -> Prop
  :=
  | WellTypedValue__boolean : forall tau e b,
      e = boolean b ->
      tau = booleanType ->
      WellTypedValue__Boolean WTV {| type := tau; expr := e |}
.

Global Instance IndexedFunctor__WellTypedValue__Boolean
       {T V}
       `{Functor T} `{Functor V}
       `{T supports BooleanType}
       `{V supports Boolean}
  : IndexedFunctor (TypedExpr T V) WellTypedValue__Boolean.
Proof.
  constructor.
  move => A B i IH [] t v b -> -> .
  econstructor => //; apply IH => //.
Qed.

(**
This is a nice-to-have inversion principle for [WellTypedValue__Boolean].  It
gives us a little bit more control than using the [inversion] tactic.
 *)
Definition WellTypedValueInversionClear__Boolean
           {T V}
           `{Functor T} `{Functor V}
           `{T supports BooleanType}
           `{V supports Boolean}
           (WellTypedValue__V : (TypedExpr T V)-indexedProp)
           (tv : TypedExpr T V)
           (P : (TypedExpr T V)-indexedPropFunctor)
           (IH : forall tau v b,
               {| type := tau; expr := v |} = tv ->
               v = boolean b ->
               tau = booleanType ->
               P WellTypedValue__V {| type := tau; expr := v |})
           (WT : WellTypedValue__Boolean WellTypedValue__V tv)
  : P WellTypedValue__V tv
  :=
    match WT in (WellTypedValue__Boolean _ p) return (p = tv -> P WellTypedValue__V tv) with
    | WellTypedValue__boolean _ tau e b P__e P__tau =>
      fun EQ => eq_ind _ (fun p => P WellTypedValue__V p) (IH _ _ _ EQ P__e P__tau) tv EQ
    end eq_refl.

Global Instance WellTypedValueProjection__Boolean
       {T V}
       `{Functor T} `{Functor V}
       `{T supports BooleanType}
       `{V supports Boolean}
       (WellTypedValue__V : (TypedExpr T V)-indexedPropFunctor)
       `{(WellTypedValue__V supports WellTypedValue__Boolean)%IndexedSubFunctor}
  : IndexedProofAlgebra
      ForWellTypedValueProjection
      WellTypedValue__Boolean
      (WellTypedValueProjectionStatement
         WellTypedValue__Boolean
         booleanType
         WellTypedValue__V
      ).
Proof.
  constructor.
  move => tv [] t v b ? ?.
  apply : (WellTypedValue__boolean _ _ _ b) => //.
Qed.

Lemma Soundness__boolean
      {T E V}
      `{Functor T} `{Functor E} `{Functor V}
      `{T supports BooleanType}
      `{E supports Boolean}
      `{V supports Boolean}
      `{V supports Stuck}

      (WTV : (TypedExpr T V)-indexedPropFunctor)
      `((WTV supports WellTypedValue__Boolean)%IndexedSubFunctor)

      `{Eval__E         : ProgramAlgebra ForEval         E (EvalResult   V)}
      `{TypeEquality__T : ProgramAlgebra ForTypeEquality T (TypeEqualityResult T)}
      `{TypeOf__E       : ProgramAlgebra ForTypeOf       E (TypeOfResult T)}

      `{! WellFormedCompoundProgramAlgebra ForEval   E Boolean}
      `{! WellFormedCompoundProgramAlgebra ForTypeOf E Boolean}
  : forall (b : bool), SoundnessStatement WTV (boolean b).
Proof.
  rewrite /SoundnessStatement.
  move => b tau.
  rewrite /typeOf /eval /boolean /=.
  rewrite /mendlerFold /injectF /=.
  rewrite /wrapF.
  rewrite wellFormedCompoundProgramAlgebra /=.
  rewrite wellFormedCompoundProgramAlgebra /=.
  move => [] <- .
  apply indexedWrapF.
  apply indexedInject.
  econstructor => //.
Defined.

Lemma Soundness__ifThenElse
      {T E V}
      `{Functor T} `{Functor E} `{Functor V}
      `{T supports BooleanType}
      `{E supports Boolean}
      `{V supports Boolean}
      `{V supports Stuck}
      (WTV : (TypedExpr T V)-indexedPropFunctor)
      `((WTV supports WellTypedValue__Boolean)%IndexedSubFunctor)
      `{Eval__E         : ProgramAlgebra ForEval         E (EvalResult V)}
      `{TypeEquality__T : ProgramAlgebra ForTypeEquality T (TypeEqualityResult T)}
      `{TypeOf__E       : ProgramAlgebra ForTypeOf       E (TypeOfResult T)}
      `{! WellFormedCompoundProgramAlgebra ForEval   E Boolean}
      `{! WellFormedCompoundProgramAlgebra ForTypeOf E Boolean}

      `{! IndexedFunctor (TypedExpr T V) WTV}

      `{! IndexedProofAlgebra
          ForWellTypedValueProjection
          WTV
          (WellTypedValueProjectionStatement WellTypedValue__Boolean
                                             booleanType
                                             WTV)
       }

      `{! ProofAlgebra
          ForTypeEqualityCorrectness
          T
          (sig TypeEqualityCorrectnessStatement)
       }

  : forall (c t e : sig (SoundnessStatement WTV)),
    let c := proj1_sig c in
    let t := proj1_sig t in
    let e := proj1_sig e in
    SoundnessStatement WTV (ifThenElse c t e).
Proof.
  rewrite {7}/SoundnessStatement /=.
  move => [c IH__c] [t IH__t] [e IH__e].
  move : IH__c IH__t IH__e.
  rewrite {1 2 3}/SoundnessStatement.
  move => IH__c IH__t IH__e.
  rewrite /eval /typeOf /ifThenElse /mendlerFold /injectF /wrapF.
  rewrite wellFormedCompoundProgramAlgebra => /=.
  rewrite wellFormedCompoundProgramAlgebra => /=.
  rewrite -/eval -/typeOf.
  case TO__c : (typeOf c) => [ tau__c | ] //.
  move : IH__c (IH__c _ TO__c) => _ WT__c.
  case BT : (isBooleanType tau__c) => //.
  case TO__t : (typeOf t) => [ tau__t | ] //.
  move : IH__t (IH__t _ TO__t) => _ WT__t.
  case TO__e : (typeOf e) => [ tau__e | ] //.
  move : IH__e (IH__e _ TO__e) => _ WT__e.
  move => tau.
  case TE : (typeEquality tau__t tau__e) => //.
  move => [] <-.
  move : BT.
  rewrite / isBooleanType.
  case p__c : (projectF tau__c) => [ [] | ] // _.
  have := !! projectF_injectF p__c => {}p__c.
  have := !! wellTypedValueProjection WellTypedValue__Boolean _ _ _ WT__c p__c.
  elim / @WellTypedValueInversionClear__Boolean.
  move => ? ? b [] -> -> -> _ .
  rewrite /isBoolean /projectF /mendlerFold.
  rewrite /boolean /injectF.
  rewrite unwrapF_wrapF.
  rewrite project_inject /=.
  move : b => [] //.
  have := !! typeEqualityCorrectness _ _ TE => -> .
  apply WT__e.
Defined.

Definition Induction__Boolean
           {E} `{Functor E} `{E supports Boolean}
           (P : Fix E -> Prop)
           (H__boolean : forall b, P (boolean b))
           (H__ifThenElse :
              forall (c t e : sig P),
                let c := proj1_sig c in
                let t := proj1_sig t in
                let e := proj1_sig e in
                P (ifThenElse c t e))
  : Algebra Boolean (sig P)
  := fun e =>
       match e with
       | MkBoolean b => exist _ _ (H__boolean b)
       | IfThenElse c t e =>
         exist _ _ (H__ifThenElse c t e)
       end.

Global Instance Soundness__Boolean
      {T E V}
      `{Functor T} `{Functor E} `{Functor V}
      `{T supports BooleanType}
      `{E supports Boolean}
      `{V supports Boolean}
      `{V supports Stuck}
      (WTV : (TypedExpr T V)-indexedPropFunctor)
      `((WTV supports WellTypedValue__Boolean)%IndexedSubFunctor)
      `{Eval__E         : ProgramAlgebra ForEval         E (EvalResult         V)}
      `{TypeEquality__T : ProgramAlgebra ForTypeEquality T (TypeEqualityResult T)}
      `{TypeOf__E       : ProgramAlgebra ForTypeOf       E (TypeOfResult       T)}

      `{! WellFormedCompoundProgramAlgebra ForEval   E Boolean}
      `{! WellFormedCompoundProgramAlgebra ForTypeOf E Boolean}

      `{! IndexedFunctor (TypedExpr T V) WTV}

      `{! IndexedProofAlgebra
          ForWellTypedValueProjection WTV
          (WellTypedValueProjectionStatement WellTypedValue__Boolean
                                             booleanType
                                             WTV)
       }

      `{! ProofAlgebra
          ForTypeEqualityCorrectness T
          (sig TypeEqualityCorrectnessStatement)
       }

  : ProofAlgebra ForSoundness
                 Boolean
                 (sig (SoundnessStatement (E := E) WTV)).
Proof.
  constructor.
  apply Induction__Boolean.

  { (* [boolean] case *)
    rewrite /SoundnessStatement.
    eapply Soundness__boolean => //.
  }

  { (* [ifThenElse] case *)
    rewrite /SoundnessStatement.
    move => c t e /=.
    move => tau TO.
    apply (Soundness__ifThenElse WTV _ c t e) => //.
  }

Defined.

BooleanType.v

From Coq Require Import
     ssreflect
.

From MTC Require Import
     Algebra
     Functor
     SubFunctor
     TypeEquality
.

Local Open Scope SubFunctor.

Inductive BooleanType (A : Set) : Set :=
| MkBooleanType : BooleanType A
.
Arguments MkBooleanType {A}.

Global Instance Functor__BooleanType
  : Functor BooleanType
  := {| fmap := fun A B f 'MkBooleanType => MkBooleanType |}.

Definition booleanType
           {T}
           `{Functor T}
           `{T supports BooleanType}
  : Fix T
  := injectF MkBooleanType.

Definition isBooleanType
           {E} `{Functor E} `{E supports BooleanType}
  : Fix E -> bool
  := fun v =>
       match projectF v with
       | Some MkBooleanType => true
       | _                  => false
       end.

Global Instance TypeEquality__BooleanType
           T `{Functor T} `{T supports BooleanType}
  : ProgramAlgebra ForTypeEquality BooleanType (TypeEqualityResult T)
  :=
    {|
      programAlgebra :=
        fun _ _ '(MkBooleanType) => fun t => isBooleanType t
      ;
    |}.

Global Instance TypeEqualityCorrectness__BooleanType
       {T} `{Functor T}
       `{! T supports BooleanType}
       `{! ProgramAlgebra ForTypeEquality T (TypeEqualityResult T)}
       `{! WellFormedCompoundProgramAlgebra ForTypeEquality T BooleanType}
  : ProofAlgebra
      ForTypeEqualityCorrectness
      BooleanType
      (sig TypeEqualityCorrectnessStatement).
Proof.
  constructor => [] [].
  exists booleanType.
  rewrite /TypeEqualityCorrectnessStatement.
  move => tau'.
  rewrite /typeEquality /mendlerFold {1} /booleanType.
  rewrite /injectF /wrapF.
  rewrite wellFormedCompoundProgramAlgebra /=.
  rewrite / isBooleanType.
  case P : (projectF tau') => [ [] | ] // => _.
  move : P.
  rewrite / projectF.
  move /project_success.
  move /(f_equal (wrapF (E := T))).
  rewrite /booleanType /injectF.
  rewrite wrapF_unwrapF => //.
Defined.

Demo.v

From Coq Require Import
     ssreflect
.

From MTC Require Import
     Algebra
     Boolean
     BooleanType
     Eval
     Functor
     IndexedAlgebra
     IndexedFunctor
     IndexedSubFunctor
     IndexedSum1
     Natural
     NaturalType
     Soundness
     SubFunctor
     Stuck
     Sum1
     TypeEquality
     TypeOf
     WellTypedValue
     WellTypedValueProjection
.

(**
We can create languages to instantiate all of our operations.
 *)

(** An extensible type language: *)
Definition TypeLanguage       := (BooleanType + NaturalType)%Sum1.

(** An extensible expression language: *)
Definition ExpressionLanguage := (Boolean + Natural)%Sum1.

(** And an extensible value language: *)
Definition ValueLanguage      := (Boolean + Natural + Stuck)%Sum1.

(** We can instantiate our operations: *)

Definition eval
  : Fix ExpressionLanguage -> EvalResult ValueLanguage
  := MTC.Eval.eval.
  (* ^ we need to fully qualify here because [Eval] is a Coq keyword... *)

Definition typeOf
  : Fix ExpressionLanguage -> TypeOfResult TypeLanguage
  := TypeOf.typeOf.

Definition WellTypedValue
  : (TypedExpr TypeLanguage ValueLanguage)-indexedPropFunctor
  := (WellTypedValue__Boolean + WellTypedValue__Natural)%IndexedSum1.

(**
Remember that [typeOf] returns an extensible type!  So it's not nice looking at,
as it is still a fold:
 *)
Compute typeOf (natural 42).

(**
If you look in there, you should see [inr1 MkNaturalType], which is the correct
answer.  But we can make it look nicer by translating into a concrete type when
we want to inspect results:
 *)

Variant InspectType :=
| InspectBooleanType
| InspectNaturalType
| InspectIllTyped
.

Definition inspectTypeOf
  : Fix ExpressionLanguage -> InspectType
  := fun e =>
       match typeOf e with
       | None   => InspectIllTyped
       | Some tau =>
         tau InspectType
           (fun _ rec =>
              (
                (fun 'MkBooleanType => InspectBooleanType)
                ||
                (fun 'MkNaturalType => InspectNaturalType)
              )%Sum1
           )
       end.

Compute inspectTypeOf (natural 42).

Variant InspectValue :=
| InspectBoolean  (b : bool)
| InspectNatural  (n : nat)
| InspectStuck    (why : Reason)
| InspectBadValue
.

Definition inspectEval
  : Fix ExpressionLanguage -> InspectValue
  := fun e =>
       eval e
            InspectValue
            (fun _ rec =>
               (
                 (fun e => match e with
                        | MkBoolean b => InspectBoolean b
                        | _           => InspectBadValue
                        end)
                 ||
                 (fun e => match e with
                        | MkNatural n => InspectNatural n
                        | _           => InspectBadValue
                        end)
                 ||
                 (fun '(MkStuck why) => InspectStuck why)
               )%Sum1
            ).

Definition someBooleanExpression
  : Fix ExpressionLanguage
  := boolean false.

Definition someNaturalExpression
  : Fix ExpressionLanguage
  := ifThenElse (boolean true)
                (plus (natural 2) (natural 3))
                (natural 4).

Definition someIllTypedExpression
  : Fix ExpressionLanguage
  := ifThenElse (boolean true)
                (plus (natural 2) (natural 3))
                (boolean false).

(**
We can now inspect the result of running [typeOf]:
 *)
Compute inspectTypeOf someBooleanExpression.
Compute inspectTypeOf someNaturalExpression.
Compute inspectTypeOf someIllTypedExpression.

(**
We can now inspect the result of running [eval]:
 *)
Compute inspectEval someBooleanExpression.
Compute inspectEval someNaturalExpression.
(* Note that [eval] does not care about well-typedness: *)
Compute inspectEval someIllTypedExpression.

Theorem Soundness
  : forall (tau : Fix TypeLanguage) (e : Fix ExpressionLanguage),
    typeOf e = Some tau ->
    IndexedFix WellTypedValue {| type := tau; expr := eval e; |}.
Proof.
  move => tau e.
  apply Soundness.
  typeclasses eauto.
Qed.

Eval.v

From MTC Require Import
     Algebra
.

(**
We will use this as an alias for the return type of the [Eval] operation.  While
it is just [Fix], the idea is that we could decide to change it later, so all
[ProgramAlebra]s should use the alias.
 *)
Definition EvalResult V := Fix V.

(** Tag for [Eval]-related [ProgramAlgebra]s *)
Variant ForEval := .

(**
The [eval] operation is defined as the fold of its [ProgramAlgebra].
 *)
Definition eval
           {E V}
           {eval__E : ProgramAlgebra ForEval E (EvalResult V)}
  : Fix E -> EvalResult V
  := mendlerFold programAlgebra.

Functor.v

Class Functor (F : Set -> Set) :=
  {
    fmap : forall {A B : Set} (f : A -> B), F A -> F B;
  }.

Hacks.v

Notation "!! x" := (ltac:(refine x)) (at level 100, only parsing).

IndexedAlgebra.v

From MTC Require Import
     IndexedFunctor
     IndexedSum1
.

Definition IndexedAlgebra
           {I} (F : I-indexedPropFunctor) (A : I-indexedProp)
  : Prop
  := forall i, F A i -> A i.

Definition IndexedMendlerAlgebra
           {I} (F : I-indexedPropFunctor) (A : I-indexedProp)
  : Prop
  := forall i (R : I -> Prop), (forall i, R i -> A i) -> F R i -> A i.

Definition IndexedFix
           {I} (F : I-indexedPropFunctor) i
  : Prop
  := forall (A : I-indexedProp), IndexedMendlerAlgebra F A -> A i.

Definition indexedMendlerFold
           {I} {F : I-indexedPropFunctor} {A : I -> Prop}
           (f : IndexedMendlerAlgebra F A) i
  : IndexedFix F i -> A i
  := fun e => e A f.

Definition indexedWrapF
           {I} {F : I-indexedPropFunctor}
           i (unwrapped : F (IndexedFix F) i)
  : IndexedFix F i
  := fun A f
     => f i (IndexedFix F) (indexedMendlerFold f) unwrapped.

Definition indexedFold
           {I} {F : I-indexedPropFunctor} {A : I-indexedProp}
           `{IndexedFunctor I F}
           (f : IndexedAlgebra F A) i (e : IndexedFix F i)
  : A i
  := indexedMendlerFold (fun i' r rec fa => f i' (indexedFmap i' rec fa)) i e.

Definition indexedUnwrapF
           {I} {F : I-indexedPropFunctor} `{IndexedFunctor I F}
  : forall (i : I), IndexedFix F i -> F (IndexedFix F) i
  := indexedFold (fun i => indexedFmap i indexedWrapF).

Class IndexedProofAlgebra
      (Tag : Set) {I} (F : I-indexedPropFunctor) A :=
  {
    indexedProofAlgebra : IndexedAlgebra F A;
  }.

Global Instance
       IndexedProofAlgebra__Sum1
       {Tag I} F G {A : I-indexedProp}
       `{! IndexedProofAlgebra Tag F A}
       `{! IndexedProofAlgebra Tag G A}
  : IndexedProofAlgebra Tag (F + G)%IndexedSum1 A
  :=
    {|
      indexedProofAlgebra :=
        fun i fg =>
          match fg with
          | iinl1 f => indexedProofAlgebra i f
          | iinr1 g => indexedProofAlgebra i g
          end
      ;
    |}.

IndexedFunctor.v

Notation "I '-indexedProp'" := (I -> Prop) (at level 50, only parsing).
Notation "I '-indexedPropFunctor'" := (I-indexedProp -> I-indexedProp) (at level 50).

Class IndexedFunctor I (F : I-indexedPropFunctor) : Prop :=
  {
    indexedFmap : forall {A B : I -> Prop} i, (forall i, A i -> B i) -> F A i -> F B i;
  }.

IndexedSubFunctor.v

From MTC Require Import
     IndexedFunctor
     IndexedSum1
.

Local Open Scope IndexedSum1.

(**
[F] is a SubFunctor of [E] when [E] is "larger" than [F].
 *)
Class IndexedSubFunctor
      {I} (F E : I-indexedPropFunctor)
  : Prop
  :=
    {
      indexedInject  : forall {A i}, F A i -> E A i;
      indexedProject : forall {A i}, E A i -> F A i \/ True;
    }.

Declare Scope IndexedSubFunctor.
Delimit Scope IndexedSubFunctor with IndexedSubFunctor.
Notation "E 'supports' F" := (IndexedSubFunctor F E) (at level 50) : IndexedSubFunctor.
Local Open Scope IndexedSubFunctor.

Global Instance IndexedSubFunctor__Refl
       {I} {F} `{IndexedFunctor I F} : IndexedSubFunctor F F :=
  {|
    indexedInject  := fun _ _ fa => fa;
    indexedProject := fun _ _ fa => or_introl fa;
  |}.

Global Instance IndexedSubFunctor__Left
       {I} {F G H}
       `{IndexedFunctor I F} `{IndexedFunctor I G} `{IndexedFunctor I H}
       `{G supports F}
  : (G + H) supports F :=
  {|
    indexedInject  := fun _ _ fa => iinl1 (indexedInject fa);
    indexedProject := fun _ _ gh =>
                        match gh with
                        | iinl1 g => indexedProject g
                        | iinr1 _ => or_intror Logic.I
                        end;
  |}.

Global Instance IndexedSubFunctor__Right
       {I} {F G H}
       `{IndexedFunctor I F} `{IndexedFunctor I G} `{IndexedFunctor I H}
       `{H supports F}
  : (G + H) supports F :=
  {|
    indexedInject  := fun _ _ fa => iinr1 (indexedInject fa);
    indexedProject := fun _ _ gh =>
                        match gh with
                        | iinl1 _  => or_intror Logic.I
                        | iinr1 ha => indexedProject ha
                        end;
  |}.

IndexedSum1.v

From MTC Require Import
     IndexedFunctor
.

Declare Scope IndexedSum1.
Delimit Scope IndexedSum1 with IndexedSum1.
Local Open Scope IndexedSum1.

Variant IndexedSum1 I (F G : I-indexedPropFunctor) (A : I-indexedProp) (i : I) : Prop :=
| iinl1 : F A i -> (F + G)%IndexedSum1 A i
| iinr1 : G A i -> (F + G)%IndexedSum1 A i
where "F + G" := (IndexedSum1 _ F G) : IndexedSum1.
Arguments iinl1 {I F G A i}.
Arguments iinr1 {I F G A i}.

Global Instance IndexedFunctorSum1
       {I} {F G : I-indexedPropFunctor} `{IndexedFunctor I F} `{IndexedFunctor I G}
  : IndexedFunctor I (F + G)
  | 0 :=
  {|
    indexedFmap
    := fun A B i f fg =>
         match fg with
         | iinl1 fa => iinl1 (indexedFmap i f fa)
         | iinr1 ga => iinr1 (indexedFmap i f ga)
         end;
  |}.

Definition indexedSum1Dispatch
           {I} {A : I -> Prop} {L R : I-indexedPropFunctor} {O : I -> Prop} {i}
           (fl : L A i -> O i) (fr : R A i -> O i) v :=
  match v with
  | iinl1 l => fl l
  | iinr1 r => fr r
  end.

Notation "f || g" := (indexedSum1Dispatch f g) : IndexedSum1.

Makefile

COQ_MAKEFILE=Makefile.coq

all: ${COQ_MAKEFILE}
	make -f ${COQ_MAKEFILE}

clean: ${COQ_MAKEFILE}
	make -f ${COQ_MAKEFILE} clean

${COQ_MAKEFILE}: _CoqProject
	coq_makefile -f _CoqProject -o $@

Natural.v

From Coq Require Import
     ssreflect
.

From MTC Require Import
     Algebra
     Eval
     Functor
     Hacks
     IndexedAlgebra
     IndexedFunctor
     IndexedSubFunctor
     NaturalType
     Soundness
     Stuck
     SubFunctor
     TypeOf
     WellTypedValue
     WellTypedValueProjection
.

Local Open Scope SubFunctor.

Inductive Natural (E : Set) : Set :=
| MkNatural (n : nat)
| Plus (m n : E)
.
Arguments MkNatural {E}.
Arguments Plus      {E}.

Global Instance Functor__Natural
  : Functor Natural
  :=
    {|
      fmap :=
        fun _ _ f v =>
          match v with
          | MkNatural n => MkNatural n
          | Plus a b    => Plus (f a) (f b)
          end
    |}.

Definition natural
           {E} `{Functor E} `{E supports Natural}
           (n : nat)
  : Fix E
  := injectF (MkNatural n).

Definition plus
           {E} `{Functor E} `{E supports Natural}
           (a b : Fix E)
  : Fix E
  := injectF (Plus a b).

Definition isNatural
           {E} `{Functor E} `{E supports Natural}
  : Fix E -> option nat
  := fun v =>
       match projectF v with
       | Some (MkNatural n) => Some n
       | _                  => None
       end.

Global Instance Eval__Natural
       {R} `{Functor R}
       `{R supports Natural}
       `{R supports Stuck}
  : ProgramAlgebra ForEval Natural (EvalResult R)
  :=
    {|
      programAlgebra :=
        fun _ rec n =>
          match n with
          | MkNatural n => natural n
          | Plus a b    =>
            match (isNatural (rec a), isNatural (rec b)) with
            | (Some na, Some nb) => natural (na + nb)
            | (None,    Some _)  => stuck LeftAddendNotNatural
            | (Some _,  None)    => stuck RightAddendNotNatural
            | (None,    None)    => stuck NeitherAddendNatural
            end
          end
    |}.

Global Instance TypeOf__Natural
       {T} `{Functor T} `{T supports NaturalType}
  : ProgramAlgebra ForTypeOf Natural (TypeOfResult T)
  :=
    {|
      programAlgebra :=
        fun _ rec v =>
          match v with
          | MkNatural _ => Some naturalType
          | Plus a b =>
            match (rec a, rec b) with
            | (Some tau__a, Some tau__b) =>
              if (isNaturalType tau__a && isNaturalType tau__b)%bool
              then Some naturalType
              else None
            | _ => None
            end
      end
      ;
    |}.

Inductive WellTypedValue__Natural
          {T E}
          `{Functor T} `{Functor E}
          `{T supports NaturalType}
          `{E supports Natural}
          (WTV : TypedExpr T E -> Prop)
  : TypedExpr T E -> Prop
  :=
  | WellTypedValue__natural : forall tau e b,
      e = natural b ->
      tau = naturalType ->
      WellTypedValue__Natural WTV {| type := tau; expr := e |}
.

Global Instance IndexedFunctor__WellTypedValue__Natural
       {T V}
       `{Functor T} `{Functor V}
       `{T supports NaturalType}
       `{V supports Natural}
  : IndexedFunctor (TypedExpr T V) WellTypedValue__Natural.
Proof.
  constructor.
  move => A B i IH [] t v n -> -> .
  econstructor => //; apply IH => //.
Qed.

(**
This is a nice-to-have inversion principle for [WellTypedValue__Natural].  It
gives us a little bit more control than using the [inversion] tactic.
 *)
Definition WellTypedValueInversionClear__Natural
           {T V}
           `{Functor T} `{Functor V}
           `{T supports NaturalType}
           `{V supports Natural}
           (WellTypedValue__V : (TypedExpr T V)-indexedProp)
           (tv : TypedExpr T V)
           (P : (TypedExpr T V)-indexedPropFunctor)
           (IH : forall tau v b,
               {| type := tau; expr := v |} = tv ->
               v = natural b ->
               tau = naturalType ->
               P WellTypedValue__V {| type := tau; expr := v |})
           (WT : WellTypedValue__Natural WellTypedValue__V tv)
  : P WellTypedValue__V tv
  :=
    match WT in (WellTypedValue__Natural _ p) return (p = tv -> P WellTypedValue__V tv) with
    | WellTypedValue__natural _ tau e b P__e P__tau =>
      fun EQ => eq_ind _ (fun p => P WellTypedValue__V p) (IH _ _ _ EQ P__e P__tau) tv EQ
    end eq_refl.

Global Instance WellTypedValueProjection__Natural
       {T V}
       `{Functor T} `{Functor V}
       `{T supports NaturalType}
       `{V supports Natural}
       (WellTypedValue__V : (TypedExpr T V)-indexedPropFunctor)
       `{(WellTypedValue__V supports WellTypedValue__Natural)%IndexedSubFunctor}
  : IndexedProofAlgebra
      ForWellTypedValueProjection
      WellTypedValue__Natural
      (WellTypedValueProjectionStatement
         WellTypedValue__Natural
         naturalType
         WellTypedValue__V
      ).
Proof.
  constructor.
  move => tv [] t v n ? ?.
  apply : (WellTypedValue__natural _ _ _ n) => //.
Qed.

Lemma Soundness__natural
      {T E V}
      `{Functor T} `{Functor E} `{Functor V}
      `{T supports NaturalType}
      `{E supports Natural}
      `{V supports Natural}
      `{V supports Stuck}

      (WTV : (TypedExpr T V)-indexedPropFunctor)
      `((WTV supports WellTypedValue__Natural)%IndexedSubFunctor)

      `{Eval__E         : ProgramAlgebra ForEval         E (EvalResult   V)}
      `{TypeOf__E       : ProgramAlgebra ForTypeOf       E (TypeOfResult T)}

      `{! WellFormedCompoundProgramAlgebra ForEval   E Natural}
      `{! WellFormedCompoundProgramAlgebra ForTypeOf E Natural}
  : forall (n : nat),
    forall tau,
      typeOf (natural n) = Some tau ->
      IndexedFix
        WTV
        {|
          type := tau;
          expr := eval (natural n);
        |}.
Proof.
  rewrite /=.
  move => n tau.
  rewrite /typeOf /eval /natural /=.
  rewrite /mendlerFold /injectF /=.
  rewrite /wrapF.
  rewrite wellFormedCompoundProgramAlgebra /=.
  rewrite wellFormedCompoundProgramAlgebra /=.
  move => [] <- .
  apply indexedWrapF.
  apply indexedInject.
  econstructor => //.
Defined.

Lemma Soundness__plus
      {T E V}
      `{Functor T} `{Functor E} `{Functor V}
      `{T supports NaturalType}
      `{E supports Natural}
      `{V supports Natural}
      `{V supports Stuck}
      (WTV : (TypedExpr T V)-indexedPropFunctor)
      `((WTV supports WellTypedValue__Natural)%IndexedSubFunctor)
      `{Eval__E : ProgramAlgebra ForEval E (EvalResult V)}
      `{TypeOf__E       : ProgramAlgebra ForTypeOf       E (TypeOfResult T)}
      `{! WellFormedCompoundProgramAlgebra ForEval   E Natural}
      `{! WellFormedCompoundProgramAlgebra ForTypeOf E Natural}

      `{! IndexedFunctor (TypedExpr T V) WTV}

      `{! IndexedProofAlgebra
          ForWellTypedValueProjection
          WTV
          (WellTypedValueProjectionStatement WellTypedValue__Natural
                                             naturalType
                                             WTV)
       }

  : forall (a b : sig (SoundnessStatement WTV)),
    let a := proj1_sig a in
    let b := proj1_sig b in
    forall tau,
      typeOf (plus a b) = Some tau ->
      IndexedFix
        WTV
        {|
          type := tau;
          expr := eval (plus a b);
        |}.
Proof.
  rewrite /=.
  move => [a IH__a] [b IH__b].
  move : IH__a IH__b.
  rewrite {1 2}/SoundnessStatement.
  rewrite /eval /typeOf /plus /mendlerFold /injectF /wrapF.
  move => IH__a IH__b.
  rewrite wellFormedCompoundProgramAlgebra => /=.
  rewrite wellFormedCompoundProgramAlgebra => /=.
  case TO__a : (mendlerFold _ a) => [ tau__a | ] //.
  move : IH__a (IH__a _ TO__a) => _ WT__a.
  case TO__b : (mendlerFold _ b) => [ tau__b | ] //.
  move : IH__b (IH__b _ TO__b) => _ WT__b.
  move => tau.
  rewrite / isNaturalType.
  case p__a : (projectF tau__a) => [ [] | ] //.
  case p__b : (projectF tau__b) => [ [] | ] //.
  move => [] <- .
  have := !! projectF_injectF p__a => {}p__a.
  have := !! projectF_injectF p__b => {}p__b.
  have := !! wellTypedValueProjection WellTypedValue__Natural _ _ _ WT__a p__a.
  elim / @WellTypedValueInversionClear__Natural.
  have := !! wellTypedValueProjection WellTypedValue__Natural _ _ _ WT__b p__b.
  elim / @WellTypedValueInversionClear__Natural.
  rewrite /isNatural /projectF /mendlerFold.
  move => ? ? n__a [] -> -> -> _ .
  move => ? ? n__b [] -> -> -> _ .
  rewrite /natural /injectF.
  rewrite ! unwrapF_wrapF.
  rewrite ! project_inject /=.
  apply indexedWrapF.
  apply indexedInject.
  econstructor => //.
Defined.

Definition Induction__Natural
           {E} `{Functor E} `{E supports Natural}
           (P : Fix E -> Prop)
           (H__natural : forall b, P (natural b))
           (H__plus :
              forall (a b : sig P)
                (IH__a : P (proj1_sig a))
                (IH__b : P (proj1_sig b))
              ,
                P (plus (proj1_sig a) (proj1_sig b)))
  : Algebra Natural (sig P)
  := fun e =>
       match e with
       | MkNatural n => exist _ _ (H__natural n)
       | Plus a b =>
         exist _ _ (H__plus _ _ (proj2_sig a) (proj2_sig b))
       end.

Global Instance Soundness__Natural
      {T E V}
      `{Functor T} `{Functor E} `{Functor V}
      `{T supports NaturalType}
      `{E supports Natural}
      `{V supports Natural}
      `{V supports Stuck}
      (WTV : (TypedExpr T V)-indexedPropFunctor)
      `((WTV supports WellTypedValue__Natural)%IndexedSubFunctor)
      `{Eval__E         : ProgramAlgebra ForEval         E (EvalResult         V)}
      `{TypeOf__E       : ProgramAlgebra ForTypeOf       E (TypeOfResult       T)}

      `{! WellFormedCompoundProgramAlgebra ForEval   E Natural}
      `{! WellFormedCompoundProgramAlgebra ForTypeOf E Natural}

      `{! IndexedFunctor (TypedExpr T V) WTV}

      `{! IndexedProofAlgebra
          ForWellTypedValueProjection WTV
          (WellTypedValueProjectionStatement WellTypedValue__Natural
                                             naturalType
                                             WTV)
       }

  : ProofAlgebra ForSoundness
                 Natural
                 (sig (SoundnessStatement (E := E) WTV)).
Proof.

  constructor.
  apply Induction__Natural.

  { (* [natural] case *)
    rewrite /SoundnessStatement.
    eapply Soundness__natural => //.
  }

  { (* [plus] case *)
    rewrite /SoundnessStatement.
    move => a b _ _ /=.
    move => tau TO.
    apply (Soundness__plus WTV _ a b) => //.
  }

Defined.

NaturalType.v

From Coq Require Import
     ssreflect
.

From MTC Require Import
     Algebra
     Functor
     SubFunctor
     TypeEquality
.

Local Open Scope SubFunctor.

Inductive NaturalType (A : Set) : Set :=
| MkNaturalType : NaturalType A
.
Arguments MkNaturalType {A}.

Global Instance Functor_NaturalType
  : Functor NaturalType
  := {| fmap := fun A B f 'MkNaturalType => MkNaturalType |}.

Definition naturalType
           {T} `{Functor T} `{T supports NaturalType}
  : Fix T
  := injectF MkNaturalType.

Definition isNaturalType
           {E} `{Functor E} `{E supports NaturalType}
  : Fix E -> bool
  := fun v =>
       match projectF v with
       | Some MkNaturalType => true
       | _                  => false
       end.

Global Instance typeEquality__NaturalType
       T `{Functor T} `{T supports NaturalType}
  : ProgramAlgebra ForTypeEquality NaturalType (TypeEqualityResult T)
  :=
    {|
      programAlgebra :=
        fun _ _ '(MkNaturalType) => fun t => isNaturalType t
      ;
    |}.

Global Instance TypeEquality__NaturalType
           T `{Functor T} `{T supports NaturalType}
  : ProgramAlgebra ForTypeEquality NaturalType (TypeEqualityResult T)
  :=
    {|
      programAlgebra :=
        fun _ _ '(MkNaturalType) => fun t => isNaturalType t
      ;
    |}.

Global Instance TypeEqualityCorrectness__NaturalType
       {T} `{Functor T} `{T supports NaturalType}
       `{ProgramAlgebra ForTypeEquality T (TypeEqualityResult T)}
       `{! WellFormedCompoundProgramAlgebra ForTypeEquality T NaturalType}
  : ProofAlgebra
      ForTypeEqualityCorrectness
      NaturalType
      (sig TypeEqualityCorrectnessStatement).
Proof.
  constructor => [] [].
  exists naturalType.
  rewrite /TypeEqualityCorrectnessStatement.
  move => tau'.
  rewrite /typeEquality /mendlerFold {1} /naturalType.
  rewrite /injectF /wrapF.
  rewrite wellFormedCompoundProgramAlgebra /=.
  rewrite / isNaturalType.
  case P : (projectF tau') => [ [] | ] // => _.
  move : P.
  rewrite /projectF.
  move /project_success.
  move /(f_equal (wrapF (E := T))).
  rewrite wrapF_unwrapF => //.
Defined.

shell.nix

{ nixpkgs ? import <nixpkgs> {}
}:
with nixpkgs;
let
  coqPackages = coqPackages_8_11;
in
mkShell {
  buildInputs = [
    coqPackages.coq
  ];
  COQBIN = "";
  name = "mtc";
}

Soundness.v

From Coq Require Import
     ssreflect
.

From MTC Require Import
     Algebra
     Eval
     Functor
     Hacks
     IndexedAlgebra
     IndexedFunctor
     TypeOf
     WellTypedValue
.

Definition SoundnessStatement
           {T E V}
           `{Functor T} `{Functor E} `{Functor V}
           (WTV : (TypedExpr T V)-indexedPropFunctor)
           `{Eval__E   : ProgramAlgebra ForEval   E (EvalResult   V)}
           `{TypeOf__E : ProgramAlgebra ForTypeOf E (TypeOfResult T)}
           (e : Fix E)
  : Prop
  := forall (tau : Fix T),
    typeOf e = Some tau ->
    IndexedFix WTV {| type := tau; expr := eval e; |}.

Variant ForSoundness := .

Theorem Soundness
        {T E V}
        `{Functor T} `{Functor E} `{Functor V}
        (WTV : (TypedExpr T V)-indexedPropFunctor)
        `{Eval__E      : ProgramAlgebra ForEval      E (EvalResult   V)}
        `{TypeOf__E    : ProgramAlgebra ForTypeOf    E (TypeOfResult T)}
        `{Soundness__E : ProofAlgebra   ForSoundness E (sig (SoundnessStatement WTV))}
  : forall (e : Fix E) (tau : Fix T),
    typeOf e = Some tau ->
    IndexedFix WTV {| type := tau; expr := eval e; |}.
Proof.
  move => e tau TO.
  rewrite /eval.
  rewrite /mendlerFold.
  have := !! (Induction e tau TO) => //.
Qed.

Stuck.v

From MTC Require Import
     Algebra
     Functor
     SubFunctor
.

Local Open Scope SubFunctor.

(**
Ideally, we'd also make this an extensible data type, or maybe use [string], but
for simplicity here, let's set things in stone.
 *)
Variant Reason :=
| IfConditionNotBoolean
| LeftAddendNotNatural
| RightAddendNotNatural
| NeitherAddendNatural
.

Inductive Stuck (E : Set) : Set :=
| MkStuck (why : Reason)
.
Arguments MkStuck {E}.

Global Instance Functor__Stuck
  : Functor Stuck
  := {| fmap := fun _ _ f '(MkStuck why) => MkStuck why |}.

Definition stuck
           {E} `{Functor E} `{E supports Stuck}
           (why : Reason)
  : Fix E
  := injectF (MkStuck why).

SubFunctor.v

From Coq Require Import
     ssreflect
.

From MTC Require Import
     Functor
.

(**
[F] is a SubFunctor of [E] when [E] is "larger" than [F].
 *)
Class SubFunctor
      F E
      `{Functor F} `{Functor E}
  :=
    {
      inject  : forall {A : Set}, F A -> E A;
      project : forall {A : Set}, E A -> option (F A);
      project_inject : forall {A} {fa : F A},
          project (inject fa) = Some fa;
      project_success : forall {A} {ea : E A} {fa : F A},
          project ea = Some fa -> ea = inject fa;
    }.
Arguments inject  {F E _ _ _ A}.
Arguments project {F E _ _ _ A}.

Declare Scope SubFunctor.
Delimit Scope SubFunctor with SubFunctor.
Notation "E 'supports' F" := (SubFunctor F E) (at level 50) : SubFunctor.
Local Open Scope SubFunctor.

Global Instance SubFunctor__Refl
       F `{Functor F}
  : F supports F.
Proof.
  refine
    {|
      inject  := fun _ x => x;
      project := fun _ x => Some x;
    |}.
  - move => //.
  - move => ??? [] //.
Defined.

Sum1.v

From Coq Require Import
     ssreflect
.

From MTC Require Import
     Functor
     SubFunctor
.

Local Open Scope SubFunctor.

Declare Scope Sum1.
Delimit Scope Sum1 with Sum1.
Local Open Scope Sum1.

Variant Sum1 (F G : Set -> Set) (A : Set) : Set :=
| inl1 : F A -> (F + G)%Sum1 A
| inr1 : G A -> (F + G)%Sum1 A
where
"F + G" := (Sum1 F G) : Sum1.
Arguments inl1 {F G A}.
Arguments inr1 {F G A}.

Global Instance Functor__Sum1
       {F G} `{Functor F} `{Functor G}
  : Functor (F + G)
  :=
    {|
      fmap :=
        fun A B f fga =>
          match fga with
          | inl1 fa => inl1 (fmap f fa)
          | inr1 ga => inr1 (fmap f ga)
          end;
    |}.

Global Instance SubFunctor__Left
       F G H
       `{Functor F} `{Functor G} `{Functor H}
       `{G supports F}
  : (G + H) supports F.
Proof.
  refine
    {|
      inject  := fun _ fa => inl1 (inject fa);
      project :=
        fun _ gh =>
          match gh with
          | inl1 g => project g
          | inr1 h => None
          end
      ;
    |}.
  {
    move => A fa.
    rewrite project_inject => //.
  }
  {
    move => ? [].
    {
      move => f fa EQ.
      rewrite (project_success EQ) => //.
    }
    {
      move => //.
    }
  }
Defined.

Global Instance SubFunctor__Right
       F G H
       `{Functor F} `{Functor G} `{Functor H}
       `{H supports F}
  : (G + H) supports F.
Proof.
  refine
    {|
      inject  := fun _ fa => inr1 (inject fa);
      project :=
        fun _ gh =>
          match gh with
          | inl1 g => None
          | inr1 h => project h
          end
      ;
    |}.
  {
    move => A fa.
    rewrite project_inject => //.
  }
  {
    move => ? [].
    {
      move => //.
    }
    {
      move => g fa EQ.
      rewrite (project_success EQ) => //.
    }
  }
Defined.

Definition sum1Dispatch
           {A} {L R : Set -> Set} {O}
           (fl : L A -> O) (fr : R A -> O) (v : (L + R)%Sum1 A)
  : O
  :=
    match v with
    | inl1 l => fl l
    | inr1 r => fr r
    end.

Notation "f || g" := (sum1Dispatch f g) : Sum1.

TypeEquality.v

From Coq Require Import
     ssreflect
.

From MTC Require Import
     Algebra
     Functor
.

(**
Because [typeEquality] is a binary operation, its return type is curried: it
expects another extensible type (a value of type [Fix T]), and returns a [bool]
indicating whether that extensible type is equal to the extensible type being
folded.
 *)
Definition TypeEqualityResult
           T
  := Fix T -> bool.

(** Tag for [TypeEquality]-related [ProgramAlgebra]s *)
Variant ForTypeEquality := .

(**
The [typeEquality] operation is defined as the fold of its [ProgramAlgebra].
 *)
Definition typeEquality
           {T}
           {typeEquality__T : ProgramAlgebra ForTypeEquality T (TypeEqualityResult T)}
  : Fix T -> TypeEqualityResult T
  := mendlerFold programAlgebra.

Definition TypeEqualityCorrectnessStatement
           {T} `{Functor T}
           {typeEquality__T : ProgramAlgebra ForTypeEquality T (TypeEqualityResult T)}
           (tau : Fix T)
  : Prop
  := forall tau',
    typeEquality tau tau' = true ->
    tau = tau'.

Variant ForTypeEqualityCorrectness := .

Lemma typeEqualityCorrectness
      {T} `{Functor T}
      {typeEquality__T :
         ProgramAlgebra ForTypeEquality T (TypeEqualityResult T)}
      `{PA : ! ProofAlgebra ForTypeEqualityCorrectness T
               (sig TypeEqualityCorrectnessStatement)}
  : forall tau, TypeEqualityCorrectnessStatement tau.
Proof.
  move => tau.
  apply (Induction tau).
Qed.

TypeOf.v

From MTC Require Import
     Algebra
.

(**
For a given extensible type [T], the [typeOf] operation will either return a
concrete type [Some tau], or will fail and return [None] if the input is
ill-typed.
 *)
Definition TypeOfResult T := option (Fix T).

(** Tag for [TypeOf]-related [ProgramAlgebra]s *)
Variant ForTypeOf := .

(**
The [typeOf] operation is defined as the fold of its [ProgramAlgebra].
 *)
Definition typeOf
           {E T}
           {typeOf__E : ProgramAlgebra ForTypeOf E (TypeOfResult T)}
  : Fix E -> TypeOfResult T
  := mendlerFold programAlgebra.

WellTypedValue.v

From MTC Require Import
     Algebra
     Functor
     IndexedAlgebra
     IndexedFunctor
.

Record TypedExpr T E : Set :=
  {
    type : Fix T;
    expr : Fix E;
  }.
Arguments type {T E}.
Arguments expr {T E}.

WellTypedValueProjection.v

From Coq Require Import
     ssreflect
.

From MTC Require Import
     Algebra
     IndexedAlgebra
     IndexedFunctor
     IndexedSubFunctor
     WellTypedValue
.

(**
[WellTypedValueProjection] states that [WellTypedValue__F] is the correct handler
for handling type [tau] that satisfies [WellTypedValue__V].  In practice,
[WellTypedValue__F] will be for a given feature, for instance
[WellTypedValue__Boolean], while [WellTypedValue__V] will be the compound well-typed
relation.  This lets us do an inversion of [WellTypedValue__V] where only the
correct well-typed relation is considered.
 *)
Definition WellTypedValueProjectionStatement
           {T V}
           (WellTypedValue__F : (TypedExpr T V)-indexedPropFunctor)
           (tau : Fix T)
           (WellTypedValue__V : (TypedExpr T V)-indexedPropFunctor)
           (tv : TypedExpr T V)
  : Prop
  := type tv = tau ->
     WellTypedValue__F (IndexedFix WellTypedValue__V) tv.

Variant ForWellTypedValueProjection := .

Definition wellTypedValueProjection
           {T V}
           (WellTypedValue__F : (TypedExpr T V)-indexedPropFunctor)
           (tau : Fix T)
           (WellTypedValue__V : (TypedExpr T V)-indexedPropFunctor)
           `{IndexedFunctor (TypedExpr T V) WellTypedValue__V}
           `{S : ! IndexedSubFunctor WellTypedValue__F WellTypedValue__V}
           `{A : ! IndexedProofAlgebra
                   ForWellTypedValueProjection
                   WellTypedValue__V
                   (WellTypedValueProjectionStatement WellTypedValue__F tau WellTypedValue__V)}
  :=  indexedFold indexedProofAlgebra.

(**
This was obtained by stating one of the goals it tries to solve, say:

IndexedProofAlgebra ForWellTypedValueProjection
  WellTypedValue__Natural
  (WellTypedValueProjectionStatement WellTypedValue__Boolean booleanType WellTypedValue)

and try and prove it as generically as possible.
 *)
Ltac wellTypedValueProjection__Other :=
  constructor;
  rewrite /IndexedAlgebra;
  move => i [];
  rewrite /WellTypedValueProjectionStatement /=;
  move => *;
  match goal with
  | [ A : @eq (Fix ?T) ?tau _
    , B : @eq (Fix ?T) ?tau _
    |- _
    ] => move : A B
  end;
  move ->;
  move /(wrapF_inversion (inject _) (inject _));
  move /(discriminate_inject _ _ _) => //.

Hint Extern 5
     (IndexedProofAlgebra ForWellTypedValueProjection _ _)
=> wellTypedValueProjection__Other : typeclass_instances.