(**************************************************************)
(*   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 mm_defs.
Require Import eill eill_mm.

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

Section MM_HALTING_EILL_PROVABILITY.

  Let f : MM_PROBLEM -> EILL_SEQUENT.
  Proof.
(* Goal: forall _ : MM_PROBLEM, EILL_SEQUENT *)
    intros (n & P & v).
(* Goal: EILL_SEQUENT *)
    exact (Sig (1,P) 0, vec_map_list v (fun p : pos n => pos2nat p), 2 * n + 1).
  Defined.

  Theorem MM_HALTS_ON_ZERO_EILL_PROVABILITY : MM_HALTS_ON_ZERO ⪯ EILL_PROVABILITY.
  Proof.
(* Goal: @reduces MM_PROBLEM EILL_SEQUENT MM_HALTS_ON_ZERO EILL_PROVABILITY *)
    exists f.
(* Goal: forall x : MM_PROBLEM, iff (MM_HALTS_ON_ZERO x) (EILL_PROVABILITY (f x)) *)
    intros (n & P & v); simpl.
(* Goal: iff (@sss_output (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) (@pair nat (vec nat n) O (@vec_zero n))) (G_eill (@Sig n (@pair nat (list (mm_instr n)) (S O) P) O) (@vec_map_list nat n v (fun p : pos n => @pos2nat n p)) (Init.Nat.add (Init.Nat.add n (Init.Nat.add n O)) (S O))) *)
    rewrite <- G_eill_mm; simpl; auto.
(* Goal: iff (@sss_output (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) (@pair nat (vec nat n) O (@vec_zero n))) (@sss_compute (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) (@pair nat (vec nat n) O (@vec_zero n))) *)
    split.
    + intros (? & _); auto.
    + split; simpl; auto.
  Qed.

End MM_HALTING_EILL_PROVABILITY.
