Library label

Require Export prog.
Require Export List.
Export ListNotations.
Require Export Bool.

Fixpoint label_in_prog (p : prog) (l : label) : bool :=
  match p with
  | {{}} ⇒ false
  | s ;; q ⇒ label_in_stmt s l || label_in_prog q l
  end
with label_in_stmt (s : stmt) (l : label) : bool :=
  match s with
  | SKIP << l' >> ⇒ Nat.eqb l l'
  | _ ::= _ << l' >> ⇒ Nat.eqb l l'
  | IFB << l' >> _ THEN p1 ELSE p2 FI ⇒ Nat.eqb l l' ||
      label_in_prog p1 l || label_in_prog p2 l
  | WHILE << l' >> _ DO p1 END ⇒ Nat.eqb l l' || label_in_prog p1 l
  | ASSERT << l' >> _ =>> _ ⇒ Nat.eqb l l'
  end.

Fixpoint list_of_labels_prog (p : prog) : list label :=
  match p with
  | {{}} ⇒ []
  | s ;; q ⇒ list_of_labels_stmt s ++ list_of_labels_prog q
  end
with list_of_labels_stmt (s : stmt) : list label :=
  match s with
  | SKIP << l >> ⇒ [l]
  | _ ::= _ << l >> ⇒ [l]
  | IFB << l >> _ THEN p1 ELSE p2 FI ⇒ l :: (list_of_labels_prog p1) ++
      (list_of_labels_prog p2)
  | WHILE << l >> _ DO p1 END ⇒ l :: (list_of_labels_prog p1)
  | ASSERT << l >> _ =>> _ ⇒ [l]
  end.

Fixpoint label_in (L : list label) (l : label) :=
  match L with
  | [] ⇒ false
  | h :: t ⇒ Nat.eqb l h || label_in t l
  end.

Lemma label_in_app :
  ∀ L1 L2 l, label_in (L1++L2) l = label_in L1 l || label_in L2 l.
Proof.
  intros. induction L1 as [| h t].
  Case "[]". reflexivity.
  Case "h :: t". simpl. destruct (Nat.eqb l h).
  - reflexivity.
  - exact IHt.
Qed.

Lemma label_in_prog_iff_in_list_of_labels : ∀ p l,
  label_in_prog p l = true ↔ label_in (list_of_labels_prog p) l = true.
Proof.
  intros p l. generalize dependent p.
  prog_cases (apply (prog_mutual_ind
    (fun p ⇒ label_in_prog p l = true ↔
      label_in (list_of_labels_prog p) l = true)
    (fun s ⇒ label_in_stmt s l = true ↔
      label_in (list_of_labels_stmt s) l = true))) Case;
    intros; simpl in *; try rewrite orb_false_r; try reflexivity.
  - Case "P_cons".
    rewrite label_in_app. rewrite 2!orb_true_iff.
    split; intros H1; destruct H1.
    + SCase "-> left". left. apply H. assumption.
    + SCase "-> right". right. apply H0. assumption.
    + SCase "<- left". left. apply H. assumption.
    + SCase "<- right". right. apply H0. assumption.
  - Case "S_ifb". rewrite label_in_app.
    destruct (Nat.eqb l l0).
    + SCase "true". reflexivity.
    + SCase "false". rewrite 2!orb_false_l. rewrite 2!orb_true_iff.
      split; intros H1; destruct H1.
      × SSCase "-> left". left. apply H. assumption.
      × SSCase "-> right". right. apply H0. assumption.
      × SSCase "<- left". left. apply H. assumption.
      × SSCase "<- right". right. apply H0. assumption.
  - Case "S_while". destruct (Nat.eqb l l0).
    + SCase "true". reflexivity.
    + SCase "false". assumption.
Qed.

Definition stmt_get_label (s : stmt) :=
  match s with
  | SKIP << l >> ⇒ l
  | _ ::= _ << l >> ⇒ l
  | IFB << l >> _ THEN _ ELSE _ FI ⇒ l
  | WHILE << l >> _ DO _ END ⇒ l
  | ASSERT << l >> _ =>> _ ⇒ l
  end.

Inductive label_inR_prog : prog → label → Prop :=
  | LIP_here : ∀ l s p, label_inR_stmt s l →
      label_inR_prog (s;;p) l
  | LIP_after : ∀ l s p, label_inR_prog p l →
      label_inR_prog (s;;p) l
with label_inR_stmt : stmt → label → Prop :=
  | LIS_skip : ∀ l, label_inR_stmt (SKIP << l >>) l
  | LIS_ass : ∀ i a l, label_inR_stmt (i ::= a << l >>) l
  | LIS_ifb_cond : ∀ l b p q,
      label_inR_stmt (IFB << l >> b THEN p ELSE q FI) l
  | LIS_ifb_l : ∀ l l' b p q,
      label_inR_prog p l →
      label_inR_stmt (IFB << l' >> b THEN p ELSE q FI) l
  | LIS_ifb_r : ∀ l l' b p q,
      label_inR_prog q l →
      label_inR_stmt (IFB << l' >> b THEN p ELSE q FI) l
  | LIS_while_cond : ∀ l b p,
      label_inR_stmt (WHILE << l >> b DO p END) l
  | LIS_while_body : ∀ l l' b p,
      label_inR_prog p l →
      label_inR_stmt (WHILE << l' >> b DO p END) l
  | LIS_assert : ∀ l l' b,
      label_inR_stmt (ASSERT << l >> b =>> l') l.

Scheme label_inR_prog_mutual_ind := Induction for label_inR_prog Sort Prop
  with label_inR_stmt_mutual_ind := Induction for label_inR_stmt Sort Prop.

Lemma label_in_prog_correct : ∀ p l,
  label_in_prog p l = true ↔ label_inR_prog p l.
Proof.
  split; intros.
  - revert dependent l. revert p.
    apply (prog_mutual_ind
      (fun p ⇒ ∀ l, label_in_prog p l = true → label_inR_prog p l)
      (fun s ⇒ ∀ l, label_in_stmt s l = true → label_inR_stmt s l));
    intros.
    + inversion H.
    + simpl in H1. apply orb_true_iff in H1. destruct H1.
      × apply LIP_here. apply H; assumption.
      × apply LIP_after. apply H0; assumption.
    + simpl in H. apply Nat.eqb_eq in H. subst. constructor.
    + simpl in H. apply Nat.eqb_eq in H. subst. constructor.
    + simpl in H1. rewrite 2!orb_true_iff in H1.
      destruct H1 as [[H1 | H1] | H1].
      apply Nat.eqb_eq in H1. subst. constructor.
      apply LIS_ifb_l. apply H; assumption.
      apply LIS_ifb_r. apply H0; assumption.
    + simpl in H0. rewrite orb_true_iff in H0. destruct H0.
      apply Nat.eqb_eq in H0. subst; constructor.
      apply LIS_while_body. apply H; assumption.
    + simpl in H. apply Nat.eqb_eq in H. subst. constructor.
  - revert p l H. apply (label_inR_prog_mutual_ind
      (fun p l H ⇒ label_in_prog p l = true)
      (fun s l H ⇒ label_in_stmt s l = true)); intros; simpl.
    + rewrite H; reflexivity.
    + rewrite H; apply orb_true_r.
    + apply Nat.eqb_refl.
    + apply Nat.eqb_refl.
    + rewrite Nat.eqb_refl. reflexivity.
    + rewrite H. rewrite orb_true_r. reflexivity.
    + rewrite H. apply orb_true_r.
    + rewrite Nat.eqb_refl. reflexivity.
    + rewrite H. apply orb_true_r.
    + apply Nat.eqb_refl.
Qed.

Lemma label_inR_prog_dec : ∀ p l,
  {label_inR_prog p l} + {¬ label_inR_prog p l}.
Proof.
  apply (prog_mutual_rect
    (fun p ⇒ ∀ l, {label_inR_prog p l} + {¬ label_inR_prog p l})
    (fun s ⇒ ∀ l, {label_inR_stmt s l} + {¬ label_inR_stmt s l})); intros.
  - right; intros contra; inversion contra.
  - pose proof (H l). destruct H1.
    + left. apply LIP_here; assumption.
    + pose proof (H0 l). destruct H1.
      × left. apply LIP_after; assumption.
      × right. intros contra. inversion contra; contradiction.
  - destruct (Nat.eq_dec l l0).
    + subst. left. constructor.
    + right. intros contra. inversion contra; contradiction.
  - destruct (Nat.eq_dec l l0).
    + subst. left. constructor.
    + right. intros contra. inversion contra; contradiction.
  - destruct (Nat.eq_dec l l0).
    + left. subst. apply LIS_ifb_cond.
    + destruct (H l0).
      × left. apply LIS_ifb_l; assumption.
      × { destruct (H0 l0).
        - left. apply LIS_ifb_r; assumption.
        - right. intros contra. inversion contra; contradiction. }
  - destruct (Nat.eq_dec l l0).
    + left. subst. apply LIS_while_cond.
    + destruct (H l0).
      × left. apply LIS_while_body; assumption.
      × right. intros contra. inversion contra; contradiction.
  - destruct (Nat.eq_dec l l1).
    + subst. left. constructor.
    + right. intros contra. inversion contra; contradiction.
Qed.

Lemma stmt_get_label_in_stmt : ∀ s,
  label_inR_stmt s (stmt_get_label s).
Proof.
  intros. destruct s; constructor.
Qed.

Inductive label_first_inR_prog : prog → label → Prop :=
  | LFP_here : ∀ s p, label_first_inR_prog (s;;p) (stmt_get_label s)
  | LFP_after : ∀ l s p, label_first_inR_prog p l →
      label_first_inR_prog (s;;p) l.

Tactic Notation "label_first_inR_prog_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "LFP_here" | Case_aux c "LFP_after" ].

Lemma label_first_label_inR_prog : ∀ p l,
  label_first_inR_prog p l → label_inR_prog p l.
Proof.
  intros. label_first_inR_prog_cases (induction H) Case; intros.
  - apply LIP_here. apply stmt_get_label_in_stmt.
  - apply LIP_after. assumption.
Qed.

Lemma label_inR_prog_seq : ∀ p1 p2 l,
  label_inR_prog (p1+;+p2) l ↔ label_inR_prog p1 l ∨ label_inR_prog p2 l.
Proof.
  intros. induction p1.
  - simpl. split; intros.
    + right; assumption.
    + destruct H; [inversion H | assumption].
  - split; intros.
    + simpl in H. inversion H.
      × left; apply LIP_here; assumption.
      × apply IHp1 in H3. { destruct H3.
        - left; apply LIP_after; assumption.
        - right; assumption. }
    + simpl. destruct H.
      × { inversion H.
        - apply LIP_here; assumption.
        - apply LIP_after. apply IHp1. left; assumption. }
      × apply LIP_after. apply IHp1. right; assumption.
Qed.

Fixpoint num_lab_prog (p : prog) : nat :=
  match p with
  | {{}} ⇒ 0
  | s;;p ⇒ (num_lab_stmt s) + (num_lab_prog p)
  end
with num_lab_stmt (s :stmt) : nat :=
  match s with
  | SKIP << _ >> ⇒ 1
  | _ ::= _ << _ >> ⇒ 1
  | IFB << _ >> _ THEN p1 ELSE p2 FI ⇒ 1 + (num_lab_prog p1) + (num_lab_prog p2)
  | WHILE << _ >> _ DO p1 END ⇒ 1 + (num_lab_prog p1)
  | ASSERT << _ >> _ =>> _ ⇒ 1
  end.

Lemma num_lab_app : ∀ p q,
  num_lab_prog (p +;+ q) = num_lab_prog p + num_lab_prog q.
Proof.
  intros. induction p.
  - Case "PM_nil". simpl. reflexivity.
  - Case "PM_cons". simpl. rewrite IHp. apply PeanoNat.Nat.add_assoc.
Qed.

Theorem num_lab_stmt_lt : ∀ s,
  num_lab_stmt s > 0.
Proof. intros; destruct s; simpl; omega.
Qed.