From Equations Require Import Equations.
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax
  common typing preservation admissible fp_red structural soundness.
Require Import algorithmic.
From stdpp Require Import relations (rtc(..), nsteps(..)).
Require Import ssreflect ssrbool.

Inductive algo_dom {n} : PTm n -> PTm n -> Prop :=
| A_AbsAbs a b :
  algo_dom a b ->
  (* --------------------- *)
  algo_dom (PAbs a) (PAbs b)

| A_AbsNeu a u :
  ishne u ->
  algo_dom a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
  (* --------------------- *)
  algo_dom (PAbs a) u

| A_NeuAbs a u :
  ishne u ->
  algo_dom (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
  (* --------------------- *)
  algo_dom u (PAbs a)

| A_PairPair a0 a1 b0 b1 :
  algo_dom a0 a1 ->
  algo_dom b0 b1 ->
  (* ---------------------------- *)
  algo_dom (PPair a0 b0) (PPair a1 b1)

| A_PairNeu a0 a1 u :
  ishne u ->
  algo_dom a0 (PProj PL u) ->
  algo_dom a1 (PProj PR u) ->
  (* ----------------------- *)
  algo_dom (PPair a0 a1) u

| A_NeuPair a0 a1 u :
  ishne u ->
  algo_dom (PProj PL u) a0 ->
  algo_dom (PProj PR u) a1 ->
  (* ----------------------- *)
  algo_dom u (PPair a0 a1)

| A_UnivCong i j :
  (* -------------------------- *)
  algo_dom (PUniv i) (PUniv j)

| A_BindCong p0 p1 A0 A1 B0 B1 :
  algo_dom A0 A1 ->
  algo_dom B0 B1 ->
  (* ---------------------------- *)
  algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1)

| A_VarCong i j :
  (* -------------------------- *)
  algo_dom (VarPTm i) (VarPTm j)

| A_ProjCong p0 p1 u0 u1 :
  ishne u0 ->
  ishne u1 ->
  algo_dom u0 u1 ->
  (* ---------------------  *)
  algo_dom (PProj p0 u0) (PProj p1 u1)

| A_AppCong u0 u1 a0 a1 :
  ishne u0 ->
  ishne u1 ->
  algo_dom u0 u1 ->
  algo_dom a0 a1 ->
  (* ------------------------- *)
  algo_dom (PApp u0 a0) (PApp u1 a1)

| A_HRedL a a' b  :
  HRed.R a a' ->
  algo_dom a' b ->
  (* ----------------------- *)
  algo_dom a b

| A_HRedR a b b'  :
  ishne a \/ ishf a ->
  HRed.R b b' ->
  algo_dom a b' ->
  (* ----------------------- *)
  algo_dom a b.


Definition fin_eq {n} (i j : fin n) : bool.
Proof.
  induction n.
  - by exfalso.
  - refine (match i , j with
            | None, None => true
            | Some i, Some j => IHn i j
            | _, _ => false
            end).
Defined.

Lemma fin_eq_dec {n} (i j : fin n) :
  Bool.reflect (i = j) (fin_eq i j).
Proof.
  revert i j. induction n.
  - destruct i.
  - destruct i; destruct j.
    + specialize (IHn f f0).
      inversion IHn; subst.
      simpl. rewrite -H.
      apply ReflectT.
      reflexivity.
      simpl. rewrite -H.
      apply ReflectF.
      injection. tauto.
    + by apply ReflectF.
    + by apply ReflectF.
    + by apply ReflectT.
Defined.


Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) :
  bool by struct h :=
  check_equal a b h with (@idP (ishne a || ishf a)) := {
    | Bool.ReflectT _ _ => _
    | Bool.ReflectF _ _ => _
    }.


  (* check_equal (VarPTm i) (VarPTm j) h := fin_eq i j; *)
  (* check_equal (PAbs a) (PAbs b) h := check_equal a b _; *)
  (* check_equal (PPair a0 b0) (PPair a1 b1) h := *)
  (*   check_equal a0 b0 _ && check_equal a1 b1 _; *)
  (* check_equal (PUniv i) (PUniv j) _ := _; *)
Next Obligation.
  simpl.
  intros ih.
Admitted.

Search (Bool.reflect (is_true _) _).
Check idP.

Definition metric {n} k (a b : PTm n) :=
  exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\
  nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k.

Search (nat -> nat -> bool).