Require Import List.

Require Import Undecidability.SemiUnification.SemiU.
From Undecidability.SemiUnification.Util Require Import Enumerable.

Require Import ssreflect ssrfun ssrbool.

Set Default Proof Using "Type".
Set Default Goal Selector "!".

Module Argument.
Definition embed_var (x: nat) := atom (to_nat (x, 0)).

Definition z (b: bool) := atom (to_nat (0, if b then 2 else 1)).

Section RU2SemiU_LU2SemiU.
  Variables s0 s1 t: term.
  Definition s' := substitute embed_var (arr s0 s1).
  Definition t0' := arr (substitute embed_var t) (z false).
  Definition t1' := arr (z true) (substitute embed_var t).

  Section Transport.
    Variables φ ψ0 ψ1 : valuation.
    Variable Hψ0 : substitute ψ0 (substitute φ s0) = substitute φ t.
    Variable Hψ1 : substitute ψ1 (substitute φ s1) = substitute φ t.

    Definition φ' : valuation := fun x =>
      match of_nat x with
      | (x, 0) => substitute embed_var (φ x)
      | (0, 1) => substitute embed_var (substitute ψ0 (substitute φ s1))
      | (0, 2) => substitute embed_var (substitute ψ1 (substitute φ s0))
      | _ => atom x
      end.

    Definition ψ0' : valuation := fun x =>
      match of_nat x with
      | (x, 0) => substitute embed_var (ψ0 x)
      | _ => atom x
      end.

    Definition ψ1' : valuation := fun x =>
      match of_nat x with
      | (x, 0) => substitute embed_var (ψ1 x)
      | _ => atom x
      end.

    Lemma substitute_φ'P {r: term} :
      substitute φ' (substitute embed_var r) = substitute embed_var (substitute φ r).
    Proof. elim: r => [[| ?] | *] /=; [by rewrite /φ' ?enumP | by rewrite /φ' ?enumP | by f_equal]. Qed.

    Lemma substitute_ψ0'P {r: term} :
      substitute ψ0' (substitute embed_var r) = substitute embed_var (substitute ψ0 r).
    Proof. elim: r => [[| ?] | *] /=; [by rewrite /ψ0' ?enumP | by rewrite /ψ0' ?enumP | by f_equal]. Qed.

    Lemma substitute_ψ1'P {r: term} :
      substitute ψ1' (substitute embed_var r) = substitute embed_var (substitute ψ1 r).
    Proof. elim: r => [[| ?] | *] /=; [by rewrite /ψ1' ?enumP | by rewrite /ψ1' ?enumP | by f_equal]. Qed.

    Lemma transport : LU2SemiU (s', t0', t1').
    Proof using φ ψ0 ψ1 Hψ0 Hψ1.
      exists φ', ψ0', ψ1'. constructor.
      - rewrite /s' /t0' /=. congr arr; rewrite ?substitute_φ'P substitute_ψ0'P ?/φ' ?enumP; by congruence.
      - rewrite /s' /t1' /=. congr arr; rewrite ?substitute_φ'P substitute_ψ1'P ?/φ' ?enumP; by congruence.
    Qed.
  End Transport.

  Section Reflection.
    Variables φ' ψ0' ψ1' : valuation.
    Variable Hψ0' : substitute ψ0' (substitute φ' s') = substitute φ' t0'.
    Variable Hψ1' : substitute ψ1' (substitute φ' s') = substitute φ' t1'.

    Lemma substitute_embed_var {ξ r} :
      substitute (fun x => ξ (to_nat (x, 0))) r = substitute ξ (substitute embed_var r).
    Proof.
      elim: r; [done | by move=> /=; congruence].
    Qed.

    Lemma reflection : RU2SemiU (s0, s1, t).
    Proof using φ' ψ0' ψ1' Hψ0' Hψ1'.
      exists (fun x => φ' (to_nat (x, 0))), ψ0', ψ1'. move: Hψ0' Hψ1'.
      rewrite ?(substitute_embed_var (ξ := φ')) /s' /t0' /t1' /=.
      move=> ? ?. constructor; by congruence.
    Qed.

  End Reflection.
End RU2SemiU_LU2SemiU.
End Argument.

Require Import Undecidability.Synthetic.Definitions.

Theorem reduction : RU2SemiU ⪯ LU2SemiU.
Proof.
  exists (fun '(s0, s1, t) => (Argument.s' s0 s1, Argument.t0' t, Argument.t1' t)).
  move=> [[? ?] ?]. constructor.
  - move=> [?] [?] [?] [? ?]. apply: Argument.transport; by eassumption.
  - move=> [?] [?] [?] [? ?]. apply: Argument.reflection; by eassumption.
Qed.