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))
end.
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)
end
end.
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)
end
)
(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
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
end.
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
end
end.
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
end
end.
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
end.
Ltac step_SN :=
match goal with |- SN _ ?C =>
nfinal C;
match goal with H: nfinal C |- _ =>
apply step_SN with H; step_simpl
end
end.
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 ]
end.
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
end.
Let huit: ExecMAdd 5 3 = 8.
End MAdd.