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

Require Import List Arith Omega.

Require Import ILL.Definitions.

Require Import utils pos vec. 
Require Import subcode sss. 
Require Import list_bool bsm_defs mm_defs mm_utils mm_comp.

Local Notation "P '/BSM/' s ↓" := (sss_terminates (@bsm_sss _) P s) (at level 70, no associativity).
Local Notation "P '/MM/' s ~~> t" := (sss_output (@mm_sss _) P s t) (at level 70, no associativity).

Section BSM_MM_HALTS_ON_ZERO.

  Let f : BSM_PROBLEM -> MM_PROBLEM.
  Proof.
(* Goal: forall _ : BSM_PROBLEM, MM_PROBLEM *)
    intros (n & i & P & v).
(* Goal: MM_PROBLEM *)
    destruct (bsm_mm_compiler_2 i P) as (Q & _).
(* Goal: MM_PROBLEM *)
    exists (2+n), Q.
(* Goal: vec nat (Init.Nat.add (S (S O)) n) *)
    exact (0##0##vec_map stack_enc v).
  Defined.

  Theorem BSM_MM_HALTS_ON_ZERO : BSM_HALTING ⪯ MM_HALTS_ON_ZERO.
  Proof.
(* Goal: @reduces BSM_PROBLEM MM_PROBLEM BSM_HALTING MM_HALTING *)
    exists f.
(* Goal: forall x : BSM_PROBLEM, iff (BSM_HALTING x) (MM_HALTING (f x)) *)
    intros (n & i & P & v); simpl.
(* Goal: iff (@sss_terminates (bsm_instr n) (vec (list bool) n) (@bsm_sss n) (@pair nat (list (bsm_instr n)) i P) (@pair nat (vec (list bool) n) i v)) (MM_HALTS_ON_ZERO (let (Q, _) := @bsm_mm_compiler_2 n i P in @existT nat (fun n : nat => @sigT (list (mm_instr n)) (fun _ : list (mm_instr n) => vec nat n)) (S (S n)) (@existT (list (mm_instr (S (S n)))) (fun _ : list (mm_instr (S (S n))) => vec nat (S (S n))) Q (@vec_cons nat (S n) O (@vec_cons nat n O (@vec_map (list bool) nat stack_enc n v)))))) *)
    destruct (bsm_mm_compiler_2 i P) as (Q & H); simpl; auto.
  Qed.

End BSM_MM_HALTS_ON_ZERO.

Section BSM_MM_HALTING.

  Let f : BSM_PROBLEM -> MM_PROBLEM.
  Proof.
(* Goal: forall _ : BSM_PROBLEM, MM_PROBLEM *)
    intros (n & i & P & v).
    destruct (bsm_mm_compiler_1 i P) as (Q & _).
(* Goal: MM_PROBLEM *)
    exists (2+n), Q.
(* Goal: vec nat (Init.Nat.add (S (S O)) n) *)
    exact (0##0##vec_map stack_enc v).
  Defined.

  Theorem BSM_MM_HALTING : BSM_HALTING ⪯ MM_HALTING.
  Proof.
(* Goal: @reduces BSM_PROBLEM MM_PROBLEM BSM_HALTING MM_HALTING *)
    exists f.
(* Goal: forall x : BSM_PROBLEM, iff (BSM_HALTING x) (MM_HALTING (f x)) *)
    intros (n & i & P & v); simpl.
(* Goal: iff (@sss_terminates (bsm_instr n) (vec (list bool) n) (@bsm_sss n) (@pair nat (list (bsm_instr n)) i P) (@pair nat (vec (list bool) n) i v)) (MM_HALTING (let (Q, _) := @bsm_mm_compiler_1 n i P in @existT nat (fun n : nat => @sigT (list (mm_instr n)) (fun _ : list (mm_instr n) => vec nat n)) (S (S n)) (@existT (list (mm_instr (S (S n)))) (fun _ : list (mm_instr (S (S n))) => vec nat (S (S n))) Q (@vec_cons nat (S n) O (@vec_cons nat n O (@vec_map (list bool) nat stack_enc n v)))))) *)
    destruct (bsm_mm_compiler_1 i P) as (Q & H); simpl; auto.
  Qed.

End BSM_MM_HALTING.



  
