peanopoly.v

Set Primitive Projections.

Require Import Coq.Unicode.Utf8.
Require Coq.Program.Basics.
Require Import Coq.Program.Equality.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.SetoidClass.
Require Import Coq.Lists.List.
Require Coq.Vectors.Fin.
Require Import Coq.Vectors.VectorDef.
Require Coq.Arith.PeanoNat Nat.
Require Coq.FSets.FMapAVL.
Require Coq.Structures.OrderedTypeEx.

Import IfNotations.
Import List.ListNotations.
Import Vector.VectorNotations.

Import EqNotations.

Module Vector.
  Fixpoint Σ {n}: (Fin.t n → nat) → nat :=
    if n is S n'
    then
      λ f, f Fin.F1 + Σ (Basics.compose f Fin.FS)
    else
      λ _, 0.

  Fixpoint build {A} {n}: (Fin.t n → A) → Vector.t A n :=
    match n with
    | S n' => λ f, f Fin.F1 :: build (Basics.compose f Fin.FS)
    | _ => λ _, []
    end.

  Lemma build_nth {A B} (x: Vector.t A B): build (Vector.nth x) = x.
  Proof.
    induction x.
    all: cbn.
    1: reflexivity.
    replace (build _) with x.
    1: reflexivity.
  Qed.

  Lemma nth_build {A B} (x: Fin.t A → B) y: Vector.nth (build x) y = x y.
  Proof.
    induction y.
    all: cbn.
    1: reflexivity.
    rewrite IHy.
    reflexivity.
  Qed.

  Definition act {A B C} (f: Fin.t B → Fin.t A) (e: Vector.t C A): Vector.t C B :=
    build (Basics.compose (Vector.nth e) f).

  Lemma act_id {A B}: ∀ x: Vector.t A B, act id x = x.
  Proof.
    intro x.
    unfold act, id.
    apply build_nth.
  Qed.

  Fixpoint Forall_Prop {n A} (P: A → Prop) (e: Vector.t A n): Prop :=
    if e is h :: t
    then
      P h ∧ Forall_Prop P t
    else
      True.

  Fixpoint Forall {n A} (P: A → Type) (e: Vector.t A n): Type :=
    if e is h :: t
    then
      prod (P h) (Forall P t)
    else
      unit.

  Fixpoint Forall_Prop_build {A} (P: A → Prop) {n} (f: Fin.t n → _) (q: Forall_Prop P (build f)) i {struct i}: P (f i).
  Proof.
    destruct i.
    - cbn in q.
      destruct q.
      auto.
    - cbn in q.
      destruct q.
      apply (Forall_Prop_build _ _ _ _ H0 i).
  Qed.

  Lemma Forall_Prop_nth {A} (P: A → Prop) {n} (e: Vector.t _ n) (q: Forall_Prop P e): ∀ i, P (e [@ i]).
  Proof.
    assert (p := Forall_Prop_build P (Vector.nth e)).
    rewrite build_nth in p.
    apply p.
    auto.
  Qed.

  Fixpoint Forall_build {A} (P: A → Type) {n} (f: Fin.t n → _) (q: Forall P (build f)) i {struct i}: P (f i).
  Proof.
    destruct i.
    - cbn in q.
      destruct q.
      auto.
    - cbn in q.
      destruct q.
      apply (Forall_build _ _ _ _ f0 i).
  Qed.

  Lemma Forall_nth {A} (P: A → Type) {n} (e: Vector.t _ n) (q: Forall P e): ∀ i, P (e [@ i]).
  Proof.
    assert (p := Forall_build P (Vector.nth e)).
    rewrite build_nth in p.
    apply p.
    auto.
  Qed.
End Vector.

Module Poly.
  Record t := finpoly { s: Set ; π: s → nat ; }.

  Module PolyNotations.
    Infix "▹" := finpoly (at level 30).
  End PolyNotations.
End Poly.
Import Poly.PolyNotations.

Module Mor.
  Import Poly.

  Record t (A B: Poly.t) :=
    mor {
        s: s A → s B ;
        π x: Fin.t (π B (s x)) → Fin.t (π A x) ;
      }.

  Arguments mor {A B}.
  Arguments s {A B}.
  Arguments π {A B}.

  Definition id A: t A A := mor id (λ _, id).
  Definition compose {A B C} (f: t B C) (g: t A B): t A C :=
    mor (Basics.compose (s f) (s g)) (λ _, Basics.compose (π g _) (π f _)).

  Module MorNotations.
    Infix "∘" := compose (at level 40, left associativity).
  End MorNotations.
End Mor.

Module Ext.
  Unset Elimination Schemes.

  Record t {P: Poly.t} {V: Set}: Set := con { tag: _ ; field: Vector.t V (Poly.π P tag) ; }.
  Arguments t: clear implicits.

  Arguments con P {V} tag &.
  Arguments tag {P V}.
  Arguments field {P V}.

  Add Printing Let t.
  Add Printing Constructor t.

  Module Import ExtNotations.
    Infix "#" := (con _) (at level 30).
  End ExtNotations.

  Definition map {P} {A B: Set} (f: A → B) (e: t P A): t P B :=
    tag e # Vector.map f (field e).

  Definition map_Poly {P Q} {A: Set} (f: Mor.t P Q) (e: t P A): t Q A :=
    Mor.s f (tag e) # Vector.act (Mor.π f (tag e)) (field e).

  Definition bimap {P Q} {A B: Set} (f: Mor.t P Q) (g: A → B) (e: t P A): t Q B :=
    Mor.s f (tag e) # Vector.act (Mor.π f (tag e)) (Vector.map g (field e)).
End Ext.

Import Ext.ExtNotations.

Module W.
  Unset Elimination Schemes.

  Inductive t {P: Poly.t}: Set := roll (e: Ext.t P t).

  Arguments t: clear implicits.
  Arguments roll {P}.

  Add Printing Let t.

  Definition unroll {P} (e: t P) :=
    let 'roll e' := e in
    e'.

  Coercion unroll: t >-> Ext.t.

  Fixpoint fold {P A} (f: Ext.t P A → A) (e: t P): A :=
    f (Ext.map (fold f) (unroll e)).

  Fixpoint map {P Q} (f: Mor.t P Q) (e: t P): t Q :=
    roll (Ext.bimap f (map f) (unroll e)).
End W.

Module Combinator.
  Import Poly.

  Definition e := unit ▹ λ _, 0.

  Definition const A := A ▹ λ _, 0.

  Definition empty := const Empty_set.
  Definition unit := const unit.

  Definition sum A B := (Poly.s A + Poly.s B) ▹ λ x,
      match x with
      | inl x => Poly.π A x
      | inr x => Poly.π B x
      end.

  Definition prod A B := (s A * s B) ▹ (λ xy, π A (fst xy) + π B (snd xy)).

  Definition Σ {A: Set} (B: A → _) := { x: A & s (B x) } ▹ (λ xy, π (B (projT1 xy)) (projT2 xy)).

  (* FIXME define indexed vectors for dependent products *)

  (* Definition exp (A: nat) (B: Poly.t): Poly.t := *)
  (*  Vector.t (s B) A ▹ Vector.Σ (π B). *)

  Module CombinatorNotations.
    Infix "·" := app (at level 30).
    Infix "+" := sum.
    Infix "*" := prod.
  End CombinatorNotations.
End Combinator.

Module Free.
  Import Combinator.
  Import CombinatorNotations.

  Definition t P A := W.t (const A + P).

  Definition map {P} {A B: Set} (f: A → B): t P A → t P B :=
    W.map
      {|
        Mor.s (x: Poly.s (const A + P)) := match x return Poly.s (const B + P) with
                                           | inl x => inl (f x)
                                           | inr x => inr x
                                           end ;
        Mor.π x := match x with
                   | inl _ => id
                   | inr _ => id
                   end
      |}.

  Definition pure {P} {A: Set} (a: A): t P A := W.roll (Ext.con (const A + _) (inl a) (Vector.nil _)).

  Definition join {P} {A: Set}: t P (t P A) → t P A.
  Proof.
    refine (W.fold (λ e, _)).
    assert (f := Ext.field e).
    destruct (Ext.tag e).
    - exact s.
    - exact (W.roll (Ext.con (const _ + P) (inr s) f)).
  Defined.

  Definition bind {P} {A B: Set} (f: A → t P B): t P A → t P B.
  Proof.
    refine (W.fold (λ e, _)).
    assert (g := Ext.field e).
    destruct (Ext.tag e).
    - exact (f s).
    - exact (W.roll (Ext.con (const _ + P) (inr s) g)).
  Defined.

  (* hack to work around type checking *)
  Definition dobind {P} {A B: Set} (e: t P A) (f: A → t P B): t P B := bind f e.

  Module FreeNotations.
    Declare Scope term_scope.
    Delimit Scope term_scope with term.

    Bind Scope term_scope with t.

    Notation "'do' n ← e0 ; e1" :=
      (dobind e0 (λ n, e1))
        (n pattern, at level 200, left associativity): term_scope.
  End FreeNotations.
End Free.

Record Signature := {
    func: Poly.t ;
    rel: Poly.t ;
  }.

Existing Class Signature.

Definition Var := Set.
Existing Class Var.

Inductive prop `{Σ: Signature} `{V:Var}: Set :=
| true
| false
| and (P Q: prop)
| or (P Q: prop)
| impl (P Q: prop)

| colim (P: Free.t (func Σ) V → prop)
| lim (P: Free.t (func Σ) V → prop)
| eq (e e': Free.t (func Σ) V)

| query (R: Ext.t (rel Σ) (Free.t (func Σ) V))
.

Arguments prop: clear implicits.

Module Import PropNotations.
  Declare Scope prop_scope.
  Delimit Scope prop_scope with prop.

  Bind Scope prop_scope with prop.

  Notation "⊤" := true : prop.
  Notation "⊥" := false : prop.

  Infix "∧" := and : prop.
  Infix "∨" := or : prop.
  Infix "→" := impl : prop.

  Notation "'∃' x .. y , P" := (colim (fun x => .. (colim (fun y => P)) ..)) : prop.
  Notation "'∀' x .. y , P" := (lim (fun x => .. (lim (fun y => P)) ..)) : prop.

  Notation "¬ P" := (impl P false) : prop.

  Infix "=" := eq : prop.
  Notation "x ≠ y" := (impl (eq x y) false) : prop.
End PropNotations.


Open Scope prop.

Fixpoint equiv {Σ V n} (x: Vector.t (Free.t (func Σ) V) n): Vector.t (Free.t (func Σ) V) n → prop Σ V :=
  match x in Vector.t _ n' return Vector.t _ n' → prop Σ V with
  | h :: t => λ y, (h = Vector.hd y) ∧ equiv t (Vector.tl y)
  | [] => λ _, ⊤
  end.

Definition Theory (Σ: Signature) := (forall V: Var, prop Σ V) -> Type.
Existing Class Theory.

Reserved Infix "⊢" (at level 90).

Inductive entail `{V:Var} `{T: Theory}: prop Σ V → prop Σ V → Prop :=
| id: Reflexive entail
| compose {A B C}: B ⊢ C → A ⊢ B → A ⊢ C

| bang P: P ⊢ ⊤
| absurd P: ⊥ ⊢ P

| fanout {P Q R}: P ⊢ Q → P ⊢ R → P ⊢ (Q ∧ R)
| π1 {P Q}: (P ∧ Q) ⊢ P
| π2 {P Q}: (P ∧ Q) ⊢ Q

| fanin {P Q R}: P ⊢ R → Q ⊢ R → P ∨ Q ⊢ R
| i1 {P Q}: P ⊢ P ∨ Q
| i2 {P Q}: Q ⊢ P ∨ Q

| curry {P Q R}:
  Q ∧ P ⊢ R →
  P ⊢ (Q → R)
| uncurry {P Q R}:
  P ⊢ (Q → R) →
  Q ∧ P ⊢ R

| colim_intro {P} e:
  P e ⊢ colim P
| colim_elim {P Q}:
  (∀ x, P x ⊢ Q) →
  colim P ⊢ Q

| lim_elim {P} e:
  lim P ⊢ P e

| lim_intro {P Q}:
  (∀ x, Q ⊢ P x) →
  Q ⊢ lim P

| refl: ⊤ ⊢ ∀ x, x = x
(* P . Id = P *)
| subst P y: (∃ x, x = y ∧ P x) ⊢ P y

| axiom {P} (X: T P): ⊤ ⊢ P _
where "P ⊢ Q" := (entail P Q).

Infix "∘" := compose (at level 30).
Infix "⊢" := entail.

Existing Instance id.

Instance entail_Transitive `{Theory} `{Var} : Transitive entail.
Proof.
  intros ? ? ? f g.
  exact (g ∘ f).
Qed.

Notation "⟨ x , y , .. , z ⟩" := (fanout .. (fanout x y) .. z).

Instance and_Proper `{Theory} `{Var}: Proper (entail ==> entail ==> entail) and.
Proof.
  intros ? ? f ? ? g.
  exact ⟨ f ∘ π1 , g ∘ π2 ⟩.
Defined.

Instance or_Proper `{Theory} `{Var}: Proper (entail ==> entail ==> entail) or.
Proof.
  intros ? ? f ? ? g.
  exact (fanin (i1 ∘ f) (i2 ∘ g)).
Defined.

Instance impl_Proper `{Theory} `{Var}: Proper (Basics.flip entail ==> entail ==> entail) impl.
Proof.
  unfold Basics.flip.
  intros ? ? f ? ? g.
  apply curry.
  rewrite f.
  rewrite <- g.
  apply uncurry.
  reflexivity.
Defined.

Instance colim_Proper `{Theory} `{Var}: Proper (pointwise_relation _ entail ==> entail) colim.
Proof.
  intros ? ? f.
  apply colim_elim.
  intro.
  rewrite f.
  apply colim_intro.
Defined.

Instance lim_Proper `{Theory} `{Var}: Proper (pointwise_relation _ entail ==> entail) lim.
Proof.
  intros ? ? f.
  apply lim_intro.
  intro.
  rewrite lim_elim.
  apply f.
Defined.

Ltac xtaut := refine (_ ∘ bang _).
Ltac xabsurd := refine (absurd _ ∘ _).

Ltac xsplit := refine ⟨ _, _ ⟩.
Ltac xcase := refine (fanin _ _).

Ltac xleft := refine (i1 ∘ _).
Ltac xright := refine (i2 ∘ _).

Ltac xfirst := refine (_ ∘ π1).
Ltac xsecond := refine (_ ∘ π2).

Ltac xcurry := refine (curry _).
Ltac xuncurry := refine (uncurry _).

Ltac xlim_elim e := refine (lim_elim e ∘ _).
Ltac xlim_intro x := refine (lim_intro (λ x, _)).

Ltac xcolim_intro e := refine (colim_intro e ∘ _).
Ltac xcolim_elim x := refine (colim_elim (λ x, _)).


Definition eval `{Theory} `{Var} {P Q: prop Σ _}: P ∧ (P → Q) ⊢ Q := uncurry (id _).

Fixpoint arguments `{Σ: Signature} `{Var} (xs: list (option (Free.t (func Σ) _))) (P: prop Σ _) :=
  match xs with
  | List.cons x List.nil =>
      match x, P with
      | Some x, lim _ => ⊤
      | None, P → _ => P
      | _, _ => ⊥
      end
  | List.cons x xs' =>
      match x, P with
      | Some e, lim P => arguments xs' (P e)
      | None, P → Q => P ∧ arguments xs' Q
      | _, _ => ⊥
      end
  | List.nil => ⊤
  end.

Fixpoint instance `{Σ: Signature} `{Var} (xs: list (option (Free.t (func Σ) _))) (P: prop Σ _) :=
  if xs is List.cons x xs'
  then
    match x, P with
    | Some e, lim P => instance xs' (P e)
    | None, _ → Q => instance xs' Q
    | _, _ => ⊤
    end
  else
    P.

Lemma spec `{Theory} `{Var} xs:
  ∀ {P: prop Σ _},
    P ∧ arguments xs P ⊢ instance xs P.
Proof.
  induction xs.
  all: cbn.
  all: intros.
  1: xfirst.
  1: reflexivity.
  destruct a, P.
  all: try (exact (bang _)).
  all: try rewrite <- IHxs.
  all: try xsplit.
  - xfirst.
    apply (lim_elim t).
  - xsecond.
    destruct xs.
    all: reflexivity.
  - destruct xs.
    1: rewrite ⟨π2, π1⟩.
    1: rewrite eval.
    1: reflexivity.
    rewrite ⟨π1 ∘ π2, π1⟩.
    exact eval.
  - destruct xs.
    all: cbn.
    1: apply bang.
    1: xsecond.
    1: xsecond.
    reflexivity.
Qed.

Lemma app `{Theory} `{Var}:
  ∀ {P: prop Σ _},
    ⊤ ⊢ P →
    ∀ xs,
      arguments xs P ⊢ instance xs P.
Proof.
  intros ? f xs.
  rewrite <- (spec xs).
  xsplit.
  2: reflexivity.
  exact (f ∘ bang _).
Qed.

Arguments app {_ _ _ P} _ xs &.

Lemma trans `{Theory} `{Var}: ⊤ ⊢ ∀ x y z, x = y → y = z → x = z.
Proof.
  xlim_intro x.
  xlim_intro y.
  xlim_intro z.
  xcurry.
  xfirst.
  xcurry.
  rewrite <- (subst (λ z, x = z) z).
  rewrite <- colim_intro.
  xsplit.
  - xfirst.
    reflexivity.
  - xsecond.
    reflexivity.
Qed.

Lemma sym `{Theory} `{Var}: ⊤ ⊢ ∀ x y, x = y → y = x.
Proof.
  xlim_intro x.
  xlim_intro y.
  xcurry.
  xfirst.
  rewrite <- (subst (λ z, z = x) y).
  rewrite <- colim_intro.
  xsplit.
  - reflexivity.
  - eassert (p := app refl [Some _]).
    cbn in p.
    rewrite <- p.
    apply bang.
Qed.

Variant PEANO := ZERO | SUCC | PLUS.

Definition peano_func := PEANO ▹ λ x, match x with
                                      | ZERO => 0
                                      | SUCC => 1
                                      | PLUS => 2
                                      end.
Definition peano_rel := Empty_set ▹ λ x, match x with end.

Definition peano :=
  {|
    func := peano_func ;
    rel := peano_rel ;
  |}.

Module Import PeanoNotations.
  Import Combinator.
  Import CombinatorNotations.
  Import Ext.ExtNotations.

  Notation "'O'" := (W.roll ((inr ZERO : Poly.s (const _ + peano_func)) # [])).
  Notation "'S' e" := (W.roll ((inr SUCC : Poly.s (const _ + peano_func)) # [e])) (at level 1).
  Notation "e + e'" := (W.roll ((inr PLUS : Poly.s (const _ + peano_func)) # [e; e'])).
End PeanoNotations.

Import Free.FreeNotations.

Fixpoint ofnat {A} (n: nat): Free.t (func peano) A :=
  if n is Datatypes.S n'
  then
    S (ofnat n')
  else
    O.

Definition PEANO_dec (x y: Poly.s (func peano)): {x = y} + {x ≠ y}.
Proof.
  decide equality.
Defined.

Existing Instance peano.

(* FIXME disallow infinite sets of axioms ? *)
Variant peano_Theory: Theory peano :=
  | axiom_S_injective: peano_Theory (λ _, ∀ x y, S x = S y → x = y)
  | axiom_S_distinct: peano_Theory (λ _, ∀ x, S x ≠ O)

  | axiom_plus_O_r: peano_Theory (λ _, ∀ x, x + O = x)
  | axiom_plus_S_r: peano_Theory (λ _, ∀ x y, x + S y = S (x + y))

  (* think over this odd axiom schema *)
  | axiom_induction P: peano_Theory (λ V,
                                      P V O →
                                      (∀ x, P V x → P V (S x)) →
                                      ∀ x, P V x)
.

Existing Instance peano_Theory.

Definition S_injective `{Var}: ⊤ ⊢ _ := axiom axiom_S_injective.
Definition S_distinct `{Var}: ⊤ ⊢ _:= axiom axiom_S_distinct.
Definition plus_O_r `{Var}: ⊤ ⊢ _:= axiom axiom_plus_O_r.
Definition plus_S_r `{Var}: ⊤ ⊢ _:= axiom axiom_plus_S_r.
Definition induction `{Var} P: ⊤ ⊢ _:= axiom (axiom_induction P).

Lemma subst_F `{Var} {x y} F: x = y ⊢ F x = F y.
Proof.
  eassert (q := subst (λ z, F z = F x → F z = F y) x).
  cbn in q.
  rewrite <- (uncurry q).
  clear q.
  rewrite <- colim_intro.
  xsplit.
  - eassert (q := app refl [Some _]).
    cbn in q.
    rewrite <- q.
    clear q.
    apply bang.
  - xsplit.
    + eassert (q := app sym [Some _; Some _; None]).
      cbn in q.
      apply q.
    + eassert (q := app refl [Some _]).
      cbn in q.
      rewrite <- q.
      clear q.
      xcurry.
      apply bang.
Qed.

Example plus_O_l `{Var}: ⊤ ⊢ ∀ x, O + x = x.
Proof.
  eassert (q := app (induction (λ _ x, O + x = x)) [None; None]).
  cbn in q.
  rewrite <- q.
  clear q.
  xsplit.
  - eassert (q := app plus_O_r [Some _]).
    cbn in q.
    apply q.
  - xlim_intro x.
    xcurry.
    xfirst.
    eassert (q := app trans [Some (O + S x); Some (S (O + x)); Some (S x); None; None]).
    cbn in q.
    rewrite <- q.
    clear q.
    xsplit.
    + eassert (q := app plus_S_r [Some O; Some x]).
      cbn in q.
      rewrite <- q.
      clear q.
      xtaut.
      reflexivity.
    + exact (subst_F (λ x, S x)).
Qed.