Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
Set Warnings "-intuition-auto-with-star".
From Coq Require Import Strings.String.
From PLF Require Import Maps.
From Coq Require Import Bool.Bool.
From Coq Require Import Arith.Arith.
From Coq Require Import Arith.EqNat.
From Coq Require Import Arith.PeanoNat. Import Nat.
From Coq Require Import Lia.
From PLF Require Export Imp.
From PLF Require Import Hoare.
From PLF Require Import Hoare2.
Set Default Goal Selector "!".

Open Scope dcom_scope.


Definition FILL_IN_HERE := <{True}>.


(* ================================================================= *)
(** ** Exercise: Two Loops *)

Definition two_loops_dec (a b c : nat) : decorated :=
  <{
    {{ True }} ->>
    {{ FILL_IN_HERE }}
      X := 0
                   {{ FILL_IN_HERE }};
      Y := 0
                   {{ FILL_IN_HERE }};
      Z := c
                   {{ FILL_IN_HERE }};
      while X <> a do
                   {{ FILL_IN_HERE }} ->>
                   {{ FILL_IN_HERE }}
        X := X + 1
                   {{ FILL_IN_HERE }};
        Z := Z + 1
                   {{ FILL_IN_HERE }}
      end
                   {{ FILL_IN_HERE }} ->>
                   {{ FILL_IN_HERE }};
      while Y <> b do
                   {{ FILL_IN_HERE }} ->>
                   {{ FILL_IN_HERE }}
        Y := Y + 1
                   {{ FILL_IN_HERE }};
        Z := Z + 1
                   {{ FILL_IN_HERE }}
      end
    {{ FILL_IN_HERE }} ->>
    {{ Z = a + b + c }}
  }>.

Theorem two_loops : forall a b c,
  outer_triple_valid (two_loops_dec a b c).
Proof.
  (* FILL IN HERE *) Admitted.