Library minski

Require Import vector.

Section Minski.

  Variables m n: nat.

  Inductive Step: Set :=
  | Incr (i: nat) (hi: i<S n) (q: nat) (hq: q<=m)
  | Test (i: nat) (hi: i<S n) (q q': nat) (hq: q<=m) (hq': q'<=m).

  Definition Minski: Set := vector Step m.

  Inductive Config: Set := config (q: nat) (hq: q<=m) (r: vector nat (S n)).

  Definition reg (C: Config) := let (_,_,r) := C in r.
  Definition state(C: Config) := let (q,_,_) := C in q.
  Lemma proof: forall C, state C <= m.

  Definition args(k: nat) (x: vector nat k) (x0: vector nat (S n)): Config :=
    config (le_O_n _) (overwrite x x0).

  Definition result(C: Config) (y: nat): Prop := y = head (reg C).

  Definition final (C: Config): Prop := state C=m.
  Definition nfinal(C: Config): Prop := state C<m.
  Definition final_dec(C: Config): {final C} + {nfinal C} :=
    match lt_eq_lt_dec (state C) m with
    | inleft (left h) => right _ h
    | inleft (right h) => left _ h
    | inright h => False_rec _ (lt_irrefl _ (le_lt_trans _ _ _ (proof C) h))

  Lemma final_nnfinal: forall C, final C -> ~nfinal C.

  Lemma deConfig: forall (C: Config) (q: nat) (r: vector nat (S n)),
    q=state C -> r=reg C -> forall h, config (q:=q) h r = C.

  Lemma reg_eq: forall q h r q' r' h', config (q:=q) h r = config (q:=q') h' r' -> r = r'.

  Lemma state_eq: forall q h r q' r' h', config (q:=q) h r = config (q:=q') h' r' -> q = q'.

End Minski.
Implicit Arguments Incr [].
Implicit Arguments Test [].
Implicit Arguments config [].
Implicit Arguments deConfig [m n].

Definition MinskiM n: Set := sigS (fun m => Minski m n).
Definition Minskim m n: Minski m n -> MinskiM n := existS (fun m => Minski m n) m.
Definition Minskim' n (M: MinskiM n) := projS2 M.
Notation "{ m }" := (Minskim m).
Notation "! M" := (Minskim' M) (at level 30).
Ltac MinskiM := unfold Minskim', Minskim, projS1, projS2.
Lemma Minskimm': forall m n (M: Minski m n), Minskim' {M}=M.

Definition MinskiS: Set := sigS MinskiM.
Definition Minskis m n (M: Minski m n): MinskiS := existS MinskiM n { M }.
Definition Minskis' (M: MinskiS) := ! (projS2 M).
Notation "[ m ]" := (Minskis m).
Notation "# M" := (Minskis' M) (at level 30).
Ltac MinskiS := unfold Minskis', Minskis, projS1, projS2.
Lemma Minskiss': forall m n (M: Minski m n), #[M]=M.

Section Machine.

  Variable MS: MinskiS.

  Definition ms: nat := projS1 (projS2 MS).
  Definition ns: nat := projS1 MS.
  Definition Ms: Minski ms ns := # MS.

  Definition step(C: Config ms ns) (H: nfinal C): Config ms ns :=
    let r := reg C in
    match get Ms (state C) H with
    | Incr i hi q' hq' => config ms ns q' hq' (change r i (S (get r i hi)))
    | Test i hi q1 q2 hq1 hq2 =>
      match get r i hi with
      | 0 => config ms ns q1 hq1 r
      | S x => config ms ns q2 hq2 (change r i x)
  Implicit Arguments step [].

  Lemma step_pirr: forall (C: Config ms ns) (H H': nfinal C), step C H = step C H'.

  Inductive transition: Config ms ns -> Config ms ns -> Prop :=
  | transition_refl: forall (C: Config ms ns), transition C C
  | step_transition: forall (C C': Config ms ns) (H: nfinal C), transition (step C H) C' -> transition C C'.

  Lemma transition_step: forall (C C': Config ms ns) (H': nfinal C'), transition C C' -> transition C (step C' H').

  Lemma transition_transition: forall C D E: Config ms ns, transition C D -> transition D E -> transition C E.

  Lemma transition_final: forall C C': Config ms ns, transition C C' -> final C -> C=C'.

  Definition NF(C C': Config ms ns) := transition C C' /\ final C'.

  Definition MinskiSem (k: nat) (x: vector nat k) (y: nat) :=
    forall x0: vector nat (S ns), exists Cf, NF (args ms x x0) Cf /\ result Cf y.

  Definition MinskiSemR r r' := transition (config _ _ _ (le_O_n _) r) (config _ _ _ (le_n _) r').

  Theorem NF_injective: forall C C1 C2: Config ms ns, NF C C1 -> NF C C2 -> C1=C2.

  Lemma MinskiSemInjective: forall (k: nat) (x: vector nat k) (y y': nat),
    MinskiSem x y -> MinskiSem x y' -> y=y'.

  Inductive SN: Config ms ns -> Prop :=
  | final_SN: forall C, final C -> SN C
  | step_SN : forall C (Hnf: nfinal C), SN (step C Hnf) -> SN C.

  Let step_lt(C C': sig SN): Prop := exists h, (proj1_sig C) = step (proj1_sig C') h.
  Infix "<-" := step_lt (at level 60).

  Let step_lt_wf: well_founded step_lt.

  Let SN_SN_step: forall (C: Config ms ns) (H: nfinal C), SN C -> SN (step C H).
  Let stepSN(C: sig SN) (H: nfinal (proj1_sig C)): sig SN := exist SN (step _ H) (SN_SN_step H (proj2_sig C)).
  Let stepSN_lt: forall (C: sig SN) (H: nfinal (proj1_sig C)), stepSN C H <- C.

  Definition execute(Co: Config ms ns)(SNCo: SN Co): sig (NF Co) :=
    well_founded_induction step_lt_wf (fun (C: sig SN) => transition Co (proj1_sig C) -> sig (NF Co))
      (fun (C: sig SN) (exec: (forall C', C' <- C -> transition Co (proj1_sig C') -> sig (NF Co))) CoC =>
         match final_dec (proj1_sig C) with
         | left H => exist (NF Co) (proj1_sig C) (conj CoC H)
         | right H => exec (stepSN C H) (stepSN_lt C H) (transition_step H CoC)
      (exist SN Co SNCo)
      (transition_refl Co).
  Implicit Arguments execute [].

  Definition execute_N N k (x: vector nat k): option nat :=
    (fix e(N: nat): Config ms ns -> option nat :=
      match N with
      | 0 => fun C => None
      | S N => fun C =>
        match final_dec C with
        | left H => Some (head (reg C))
        | right H => e N (step C H)
      end) N (args _ x (fill _ (nnil _) 0)).

  Theorem MinskiSem_SN: forall k (x: vector nat k) y, MinskiSem x y -> forall x0, SN (args ms x x0).

  Lemma transition_step': forall A B C (HB: nfinal B), transition A B -> C = step B HB -> transition A C.

  Lemma step_transition': forall A B C (HA: nfinal A), B = step A HA -> transition B C -> transition A C.

  Lemma transition_eq_transition: forall A B C D, B=C -> transition A B -> transition C D -> transition A D.

  Lemma transition_refl': forall q r h q' r' h', q=q' -> r=r' -> transition (config _ _ q h r) (config _ _ q' h' r').

End Machine.

Lemma SemR: forall m n (M: Minski m n) k (x: vector nat k) y,
  (forall x0: vector nat (S n), exists r': vector nat (S n), MinskiSemR [M] (overwrite x x0) r' /\ y = head r') ->
  MinskiSem [M] x y.

Ltac msns := unfold ms, ns, projS1, projS2; simpl.
Ltac msnsH H := unfold ms, ns, projS1, projS2 in H; simpl in H.
Ltac MsNs M m n := change (ms [M]) with m; change (ns [M]) with n.
Ltac MsNsH M m n H := change (ms [M]) with m in H; change (ns [M]) with n in H.

Ltac final := unfold final; unfold state; reflexivity.
Ltac nfinal C :=
  (cut (nfinal C)); [ intro | unfold nfinal; unfold state; auto with arith ].
Ltac step_simpl := unfold step; msns.

Ltac transition_step C :=
  nfinal C; unfold MinskiSemR;
  match goal with H: nfinal C |- transition _ _ _ =>
    apply transition_step' with C H; [ step_simpl | auto ];
    try clear H

Ltac step_transition :=
  unfold MinskiSemR;
  match goal with |- transition ?M ?C _ =>
    nfinal C;
    match goal with H: nfinal C |- _ =>
      apply step_transition' with (step M C H) H; [ auto | try step_simpl ];
      try clear H

Ltac step_transition_tac tac :=
  unfold MinskiSemR;
  match goal with |- transition [?M] ?C _ =>
    nfinal C;
    match goal with H: nfinal C |- _ =>
      apply step_transition with H;
      unfold step, state, Ms, M; rewrite Minskiss';
      try rewrite tac; fold M; msns;
      try clear H

Ltac transition_refl :=
  unfold MinskiSemR;
  match goal with
  | |- transition ?M (config ?m ?n _ _ _) _ =>
    change m with (ms M); change n with (ns M);
    apply transition_refl'; auto
  | |- transition ?M _ (config ?m ?n _ _ _) =>
    change m with (ms M); change n with (ns M);
    apply transition_refl'; auto
  | |- transition _ _ _ => apply transition_refl'; auto

Ltac step_SN :=
  match goal with |- SN _ ?C =>
    nfinal C;
    match goal with H: nfinal C |- _ =>
      apply step_SN with H; step_simpl
Ltac final_SN := apply final_SN; final.

Ltac NF tac := split; [ apply tac; auto | final ].

Ltac MinskiSem r :=
  match goal with |- MinskiSem ?MS _ _ =>
    exists (config (ms MS) (ns MS) _ (le_n _) r); split;
    [ split;
      [ unfold args; try rewrite overwrite_full; msns | final ]
    | unfold result, reg; vauto ]

Ltac ElimMinskiSem H r H1 H2 :=
  elim H; intros C_ HC_; destruct C_ as [q_ hq_ r];
  elim HC_; clear HC_; intros H1 H2; elim H1; clear H1; intros H1 Hf_;
  unfold final, state in Hf_; subst;
  unfold result, reg in H2; rewrite head_get in H2; unfold args in H1;
  generalize (le_pirr hq_ (le_n _)); intro; subst.

Section MAdd.

  Definition MAdd: MinskiS.

  Theorem MAddSem: forall m n: nat, MinskiSem MAdd (m::n::nnil _) (m+n).

  Let MAddSN: forall m n: nat, SN MAdd (config 2 1 0 (le_O_n _) (m::n::nnil _)).

  Definition ExecMAdd(m n: nat): nat :=
    match execute MAdd (config 2 1 0 (le_O_n _) (m::n::nnil _)) (MAddSN m n) with
    | exist (config _ _ r) _ => head r

  Let huit: ExecMAdd 5 3 = 8.

End MAdd.