# 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. ```