Set Implicit Arguments.
Require Import List Lia.
From Undecidability.HOU Require Import std.std axioms.
Import ListNotations.

Set Default Proof Using "Type".

Section Motivation.

  Variable (n: ).
  Implicit Type (m p: ) (M N: list ( * )).

  Definition step '(a, b) := (n + a, 1 + b).
  Notation Step X := (map step X).
  Definition t k := (k * n, k).
  Definition T k := tab t k.
  Definition Mrel m p M := M [(p, m)] = t 0 :: Step M.


  Lemma step_t k: step (t k) = t (S k).
  Proof. reflexivity. Qed.

  Lemma M_forward m: Mrel m (m * n) (T m).
  Proof.
    unfold Mrel, T; change (_ _) with (tab t (S m)).
    now rewrite tab_S, tab_map.
  Qed.


  Lemma M_backward_exists m p M: Mrel m p M l, M = T l.
  Proof.
    enough ( a b x, M [x] = (a, b) :: Step M M [x] = tab ( k (a + k * n, b + k)) (S (length M))) as H.
    - intros % H; apply app_injective_right in as [ _]; eauto.
    - induction M as [|[l r]]; [cbn|]; intros; simplify; eauto.
      injection H as ? ? ; subst. specialize (IHM _ _ _ ) as .
      cbn [length]; rewrite !tab_S; cbn; simplify; do 2 f_equal.
      f_equal; . eapply tab_ext; intros; f_equal; .
  Qed.


  Lemma M_backward_equations m p l : Mrel m p (T l) m = l m * n = p.
  Proof.
    unfold Mrel. rewrite M_forward.
    intros H % app_injective; intuition; congruence.
  Qed.


  Lemma M_iff m p M: (m * n = p M = T m) Mrel m p M.
  Proof.
    split.
    - intros [ ]. apply M_forward.
    - intros H. specialize (M_backward_exists H) as [l ].
      eapply M_backward_equations in H; intuition.
  Qed.


End Motivation.