Mostly for my own benefit: some results about bounded height domains. Double-checking [calculations for an article](https://github.com/aspiwack/topocircuit)

BoundedHeightDomain.coq

Require Coq.Setoids.Setoid.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
Require Import Coq.micromega.Psatz.

(** Chains of finite length *)

Definition Chain {A} (R:A->A->Prop) (n:nat) : Type :=
  { c:{ k | k <= n } -> A |
    forall k₁ k₂, proj1_sig k₁ <= proj1_sig k₂ -> R (c k₁) (c k₂) }
.

(** BHD stands for "Bounded Height Domain" *)
Record BHD := {
  El :> Type;

  leq : El -> El -> Prop;
  leq_preorder : PreOrder leq;
  leq_ordering : PartialOrder eq leq;

  bot : El;
  bot_is_bottom : forall x, leq bot x;

  bound : nat;
  bound_is_bound : forall n, bound <= n ->
    forall c:Chain leq n, { i:_ & {j:_ | proj1_sig i< proj1_sig j &
                                         proj1_sig c i = proj1_sig c j } }
}.
Existing Instance leq_preorder.
Existing Instance leq_ordering.
Hint Immediate bot_is_bottom.
Notation "a ⩽ b" := (leq _ a b) (at level 70, no associativity).
Notation "⊥" := (bot _).

Record Increasing (A B:BHD) := {
  map :> A -> B;
  increasing : Proper (leq A ==> leq B) map
}.
Existing Instance increasing.
Notation "A ⟶ B" := (Increasing A B) (at level 99, right associativity, B at level 200).

(** Fixed points *)
Definition fixpoint {A} (f:A⟶A) (x:A) := f x = x.
Definition prefixpoint {A} (f:A⟶A) (x:A) := f x ⩽ x.

(** Fixed-point property *)

Fixpoint iter {A:BHD} (f:A⟶A) (n:nat) (a:A) : A :=
  match n with
  | 0 => a
  | S n' => iter f n' (f a)
  end
.

Lemma iter_spec :
  forall A (f:A⟶A) (n:nat) a, iter f (S n) a = f (iter f n a).
Proof.
  intros A f n.
  induction n as [|n hn].
  { reflexivity. }
  cbn. eauto.
Qed.

Lemma iter_increasing : forall A (f:A⟶A) (k₁ k₂:nat) a,
  a⩽f a -> k₁<=k₂ -> iter f k₁ a ⩽ iter f k₂ a.
Proof.
  intros A f k₁ k₂ a h hk.
  assert (k₂ = k₁ + (k₂-k₁)) as -> by lia.
  generalize (k₂-k₁); intros k'. clear -h. revert a h.
  induction k₁ as [|k hk]; cycle 1.
  { cbn. intros a h.
    apply hk.
    now apply increasing. }
  cbn.
  induction k' as [|k' hk'].
  { reflexivity. }
  cbn. intros a h.  
  transitivity (f a).
  { eauto. }
  apply hk'.
  now apply increasing.
Qed.

Program Definition iter_chain {A:BHD} (f:A⟶A) (n:nat) (a:A) (h:a⩽f a) : Chain (leq A) n :=
  fun k => iter f k a.
Next Obligation.
  eauto using iter_increasing.
Qed.

Program Definition mu {A:BHD} (f:A⟶A) : A :=
  iter f (projT1 (bound_is_bound _ _ _ (iter_chain f (A.(bound)) ⊥ _))) ⊥.

Theorem mu_fixpoint :
  forall (A:BHD) (f:A⟶A), fixpoint f (mu f).
Proof.
  intros A f. unfold mu.
  lazymatch goal with
  | |- context[projT1 ?b] => destruct b as [[i ii] [[j ji] h₀]]; cbn in *
  end.
  unfold fixpoint.
  rewrite <- iter_spec.
  enough (forall k, i<=k<=j -> iter f k ⊥ = iter f i ⊥) as l.
  { apply l. lia. }
  intros k [ik kj].
  apply antisymmetry.
  1: rewrite e.
  all: apply iter_increasing.
  all: eauto.
Qed.

Theorem mu_least_prefixpoint :
  forall (A:BHD) (f:A⟶A) (x:A), prefixpoint f x ->  mu f ⩽ x.
Proof.
  intros A f x hx.
  unfold mu.
  match goal with
  | |- context [iter f ?i] => generalize i; intros n
  end.
  induction n as [|i hi].
  + cbn. apply bot_is_bottom.
  + rewrite iter_spec.
    rewrite hi.
    apply hx.
Qed.

Corollary mu_least_fixpoint :
  forall (A:BHD) (f:A⟶A) (x:A), fixpoint f x ->  mu f ⩽ x.
Proof.
  intros * h.
  apply mu_least_prefixpoint. unfold fixpoint,prefixpoint in *.
  now rewrite h.
Qed.

Instance eq_eq_sym A B : Symmetric (@eq A ==> @eq B)%signature.
Proof.
  intros x y h. unfold respectful in *.
  firstorder congruence.
Qed.

Lemma mu_extensional (A:BHD) (f g:A⟶A) :
  (eq ==>eq )%signature f g -> mu f = mu g.
Proof.
  enough (forall f g:A⟶A, (eq==>eq)%signature f g -> mu f ⩽ mu g).
  { intros h₁. pose proof h₁ as h₂. apply symmetry in h₂.
    apply antisymmetry.
    all: eauto. }
  clear. unfold respectful. intros f g h.
  apply mu_least_fixpoint. unfold fixpoint.
  rewrite <- mu_fixpoint at 2.
  apply h. reflexivity.
Qed.

Lemma mu_increasing (A:BHD) (f g:A⟶A) :
  (leq A ==> leq A)%signature f g -> mu f ⩽ mu g.
Proof.
  unfold respectful. intros h.
  apply mu_least_prefixpoint. unfold prefixpoint.
  rewrite <- mu_fixpoint at 2.
  apply h. reflexivity.
Qed.


(** Cartesian product *)

Program Definition Product (A B:BHD) : BHD := {|
  El := A*B;
  leq x y := fst x ⩽ fst y /\ snd x ⩽ snd y;
  bot := (⊥,⊥);
  bound := A.(bound) * B.(bound)
|}.
Next Obligation.
  split.
  + intros [x y]. cbn. intuition.
  + intros [x₁ y₁] [x₂ y₂] [x₃ y₃] [h₁₁ h₁₂] [h₂₁ h₂₂].
    split.
    all:etransitivity.
    all:eauto.
Qed.
Next Obligation.
  intros [x₁ y₁] [x₂ y₂]. unfold Basics.flip. cbn. split.
  + intros [=-> ->]. intuition.
  + intros. f_equal.
    all:apply antisymmetry.
    all:intuition.
Qed.
Next Obligation.
Admitted.
Notation "A × B" := (Product A B) (at level 40, left associativity).

Instance pair_proper (A B:BHD) : Proper (leq A ==> leq B ==> leq (A×B)) pair.
Proof.
  intros x₁ x₂ hx y₁ y₂ hy. cbn.
  rewrite hx,hy. intuition.
Qed.

Instance fst_proper (A B:BHD) : Proper (leq (A×B) ==> leq A) fst.
Proof.
  intros [x₁ y₁] [x₂ y₂] h. cbn in *.
  tauto.
Qed.

Instance snd_proper (A B:BHD) : Proper (leq (A×B) ==> leq B) snd.
Proof.
  intros [x₁ y₁] [x₂ y₂] h. cbn in *.
  tauto.
Qed.

(** Parametric fixed point *)
Program Definition mup {A X:BHD} (f:A×X⟶X) : A⟶X := {|
map a := mu ({| map x := f (a,x) |})
|}.
Next Obligation.
  intros x₁ x₂ ->.
  reflexivity.
Qed.
Next Obligation.
  intros a₁ a₂ h.
  apply mu_least_prefixpoint. unfold prefixpoint. cbn.
  rewrite h. rewrite <- mu_fixpoint at 2. cbn.
  reflexivity.
Qed.

Module NaturalityInA.

  Parameters A B X : BHD.
  Parameter (f:A×X⟶X) (g:B⟶A).
  Parameter b:B.

  Program Definition lhs :=
    mu {| map x := f(g(b),x) |}.
  Next Obligation.
    intros x₁ x₂ ->. reflexivity.
  Qed.

  Program Definition rhs :=
    mu {| map x := f(g(b),x) |}.
  Next Obligation.
    intros x₁ x₂ ->. reflexivity.
  Qed.

  Lemma l : lhs = rhs.
  Proof.
    unfold lhs,rhs.
    apply mu_extensional. unfold respectful. cbn.
    intros x ? <-. reflexivity.
  Qed.

End NaturalityInA.

Module NaturalityInX.

  Parameters A X Y : BHD.
  Parameter (f:A×X⟶Y) (g:Y⟶X).
  Parameter a:A.

  Program Definition lhs :=
    mu {| map x := g (f(a,x)) |}.
  Next Obligation.
    intros x y ->. reflexivity.
  Qed.

  Program Definition rhs :=
    g (mu {| map y := f (a,g y) |}).
  Next Obligation.
    intros x y ->. reflexivity.
  Qed.

  Lemma l : lhs = rhs.
  Proof.
    unfold lhs,rhs.
    apply antisymmetry.
    + apply mu_least_fixpoint. unfold fixpoint. cbn.
      f_equal.
      rewrite <- mu_fixpoint at 2. cbn. reflexivity.
    + rewrite <- (mu_fixpoint X). cbn.
      apply increasing.
      apply mu_least_fixpoint. unfold fixpoint. cbn.
      repeat f_equal.
      rewrite <- mu_fixpoint at 2. cbn. reflexivity.
  Qed.

End NaturalityInX.

Module Bekič.

  Parameters A X Y : BHD.
  Parameters (f:A×X×Y ⟶ X) (g:A×X×Y ⟶ Y).
  Parameter a:A.

  Program Definition h :=
    mu {| map x := f (a , x , mu {| map y := g (a , x , y) |}) |}.
  Next Obligation.
    intros y z h.
    apply increasing. apply pair_proper.
    + reflexivity.
    + assumption.
  Qed.
  Next Obligation.
    intros x₁ x₂ h.
    apply increasing. apply pair_proper.
    + rewrite h. reflexivity.
    + apply mu_increasing. unfold respectful. cbn.
      intros y₁ y₂ h'.
      apply increasing. apply pair_proper.
      * rewrite h. reflexivity.
      * assumption.
  Qed.
  Arguments h : simpl never.

  Lemma h_spec pr :
    f (a , h , mu {| map y := g (a , h , y) ; increasing := pr |}) = h.
  Proof.
    unfold h at 3. rewrite <- (mu_fixpoint X). cbn.
    do 2 f_equal.
    apply mu_extensional. unfold respectful. cbn.
    intros x ? <-. reflexivity.
  Qed.
    

  Program Definition lhs :=
    mu {| map := fun (xy:X×Y) =>
                   ( f (a,fst xy,snd xy) , g (a,fst xy,snd xy) ) |}.
  Next Obligation.
    intros x y [h₁ h₂].
    split.
    all:repeat apply increasing.
    all:apply pair_proper.
    all:rewrite ?h₁,?h₂.
    all:reflexivity.
  Qed.

  Definition x₀ := fst lhs.
  Definition y₀ := snd lhs.

  Lemma x₀_spec : x₀ = f (a,x₀,y₀).
  Proof.
    unfold x₀ at 1, lhs.
    rewrite <- mu_fixpoint. cbn.
    reflexivity.
  Qed.

  Lemma y₀_spec : y₀ = g (a,x₀,y₀).
  Proof.
    unfold y₀ at 1, lhs.
    rewrite <- mu_fixpoint. cbn.
    reflexivity.
  Qed.

  Lemma lhs_spec : lhs = (x₀,y₀).
  Proof.
    unfold x₀,y₀.
    now destruct lhs.
  Qed.

  Program Definition rhs :=
    ( h , mu {| map y := g (a,h,y) |} ).
  Next Obligation.
    intros x y heq.
    apply increasing. apply pair_proper.
    + reflexivity.
    + assumption.
  Qed.

  Lemma l : lhs = rhs.
  Proof.
    unfold rhs.
    apply antisymmetry.
    + apply mu_least_fixpoint. unfold fixpoint. cbn.
      f_equal.
      * apply h_spec.
      * rewrite <- mu_fixpoint at 2. reflexivity.
    + rewrite <- mu_fixpoint, lhs_spec.
      assert (h⩽x₀) as hx₀.
      { unfold h.
        apply mu_least_prefixpoint. unfold prefixpoint. cbn.
        rewrite x₀_spec at 3.
        apply increasing.
        apply pair_proper.
        { reflexivity. }
        apply mu_least_fixpoint. unfold fixpoint. cbn.
        now rewrite <- y₀_spec. }
      apply pair_proper.
      * assumption.
      * cbn. rewrite y₀_spec.
        apply increasing.
        apply pair_proper.
        - now rewrite hx₀.
        - cbn.
          apply mu_least_prefixpoint. unfold prefixpoint. cbn.
          rewrite y₀_spec at 2.
          apply increasing.
          apply pair_proper.
          { now rewrite hx₀. }
          { reflexivity. }
  Qed.

End Bekič.