NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library multi_zero_termination

Require Import ssreflect ssrbool eqtype.
Require Import ZArith_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
Require Import mips_cmd mips_tactics mips_contrib.
Import expr_m.
Require Import multi_zero_prg.

Local Open Scope machine_int_scope.
Local Open Scope mips_expr_scope.
Local Open Scope mips_cmd_scope.

Lemma termination_multi_zero : forall s h k z ext M_,
  nodup (ext :: k :: M_ :: z :: r0 :: nil) ->
  { si | Some (s, h) -- multi_zero k z ext M_ ---> si }.
Proof.
move=> s h k z ext M_ Hset.
rewrite /multi_zero.
apply exists_addiu_seq.
rewrite sext_0 add_0.
apply exists_addiu_seq.
rewrite sext_0 add_0.
repeat reg_upd.
set s0 := store.upd _ _ _.
have [next Hext] : { kext | u2Z [ext]_s0 = Z_of_nat kext }.
  have [zext Hext] : { zext | u2Z ([ext]_s0) = zext} by eapply exist; reflexivity.
  have : 0 <= zext by rewrite -Hext; apply min_u2Z.
  case/Z_of_nat_complete_inf => next Hzext.
  by exists next; rewrite -Hzext.
move: next s0 Hext h; elim.
- move=> s0 Hext h.
  eapply exist.
  apply while.exec_while_false => /=.
  by rewrite negb_involutive store.get_r0 u2Z_Z2u // Hext.
- move=> next IH s0 Hext h; apply exists_while.
  + by rewrite /= store.get_r0 u2Z_Z2u // Hext.
  + apply exists_seq_P2 with (fun st, u2Z [ext]_(fst st) = Z_of_nat next).
    * exists_sw_P l Hl z0 Hz0.
      apply exists_addiu_seq_P.
      apply exists_addiu_P.
      rewrite /=.
      repeat reg_upd.
      rewrite sext_Z2s // u2Z_add_Z2s // Hext Z_S -Zplus_assoc /= Zplus_comm //=; by apply Zle_0_nat.
    * move=> [ si hi ] Hsi.
      by apply IH.
Qed.