(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*             Yannick Forster            [+]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(*                             [+] Affiliation Saarland Univ. *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

(** ** MM reduces to FRACTRAN *)

Require Import List Arith Omega.

Require Import ILL.Definitions.

Require Import pos vec.
Require Import sss subcode mm_defs.
Require Import fractran_defs prime_seq mm_fractran.

Set Implicit Arguments.

(** Given a FRACTRAN program and a starting state, does it terminate *)

Definition FRACTRAN_PROBLEM := (list (nat*nat) * nat)%type.

Definition FRACTRAN_HALTING (P : FRACTRAN_PROBLEM) : Prop.
Proof.
(* Goal: Prop *)
  destruct P as (l & x).
(* Goal: Prop *)
  exact (l /F/ x ↓).
Defined.

(** Given a FRACTRAN program and a starting vector [v1,...,vn],
    does the program terminate starting from p1 * q1^v1 * ... qn^vn *)

Definition FRACTRAN_ALT_PROBLEM := (list (nat*nat) * { n : nat & vec nat n })%type.

Definition FRACTRAN_ALT_HALTING : FRACTRAN_ALT_PROBLEM -> Prop.
Proof.
(* Goal: forall _ : FRACTRAN_ALT_PROBLEM, Prop *)
  intros (l & n & v).
(* Goal: Prop *)
  exact (l /F/ ps 1 * exp 1 v ↓).
Defined.

Section MM_HALTING_FRACTRAN_ALT_HALTING.

  Let f : MM_PROBLEM -> FRACTRAN_ALT_PROBLEM.
  Proof.
(* Goal: forall _ : MM_PROBLEM, FRACTRAN_ALT_PROBLEM *)
    intros (n & P & v); red.
(* Goal: prod (list (prod nat nat)) (@sigT nat (fun n : nat => vec nat n)) *)
    destruct (mm_fractran_n P) as (l & H1 & _).
(* Goal: prod (list (prod nat nat)) (@sigT nat (fun n : nat => vec nat n)) *)
    split. 
    + exact l. 
    + exists n; exact v.
  Defined.

  Theorem MM_FRACTRAN_ALT_HALTING : MM_HALTING ⪯ FRACTRAN_ALT_HALTING.
  Proof.
(* Goal: @reduces MM_PROBLEM FRACTRAN_ALT_PROBLEM MM_HALTING FRACTRAN_ALT_HALTING *)
    exists f; intros (n & P & v); simpl.
(* Goal: iff (@sss_terminates (mm_instr n) (vec nat n) (@mm_sss n) (@pair nat (list (mm_instr n)) (S O) P) (@pair nat (vec nat n) (S O) v)) (FRACTRAN_ALT_HALTING (let (l, a) := @mm_fractran_n n P in match a with | conj H1 _tmp => @pair (list (prod nat nat)) (@sigT nat (fun n : nat => vec nat n)) l (@existT nat (fun n : nat => vec nat n) n v) end)) *)
    destruct (mm_fractran_n P) as (l & H1 & H2); simpl; auto.
  Qed.

End MM_HALTING_FRACTRAN_ALT_HALTING.

Section FRACTRAN_ALT_HALTING_HALTING.

  Let f : FRACTRAN_ALT_PROBLEM -> FRACTRAN_PROBLEM.
  Proof.
(* Goal: forall _ : FRACTRAN_ALT_PROBLEM, Prop *)
    intros (l & n & v).
    exact (l,(ps 1 * exp 1 v)).
  Defined.

  Theorem FRACTRAN_ALT_HALTING_HALTING : FRACTRAN_ALT_HALTING ⪯ FRACTRAN_HALTING.
  Proof. 
(* Goal: @reduces FRACTRAN_ALT_PROBLEM FRACTRAN_PROBLEM FRACTRAN_ALT_HALTING FRACTRAN_HALTING *)
    exists f; intros (n & P & v); simpl; tauto.
  Qed.

End FRACTRAN_ALT_HALTING_HALTING.

Corollary MM_FRACTRAN_HALTING : MM_HALTING ⪯ FRACTRAN_HALTING.
Proof.
  eapply reduces_transitive. apply MM_FRACTRAN_ALT_HALTING.
  exact FRACTRAN_ALT_HALTING_HALTING.
Qed.

Check MM_FRACTRAN_HALTING.
Print Assumptions MM_FRACTRAN_HALTING.
