Library quotient

Require Export prog.
Require Import label.

Inductive is_quotientR_prog : prog → prog → Prop :=
  | IQP_nil : is_quotientR_prog {{}} {{}}
  | IQP_remove : ∀ s p q, is_quotientR_prog p q → is_quotientR_prog (s;;p) q
  | IQP_stmt : ∀ s s' p q, is_quotientR_prog p q → is_quotientR_stmt s s' →
      is_quotientR_prog (s;;p) (s';;q)
with is_quotientR_stmt : stmt → stmt → Prop :=
  | IQS_skip : ∀ l, is_quotientR_stmt (SKIP << l >>) (SKIP << l >>)
  | IQS_ass : ∀ i a l, is_quotientR_stmt (i ::= a << l >>)
                                              (i ::= a << l >>)
  | IQS_ifb : ∀ l b p1 q1 p2 q2,
      is_quotientR_prog p1 q1 → is_quotientR_prog p2 q2 →
      is_quotientR_stmt (IFB << l >> b THEN p1 ELSE p2 FI)
                        (IFB << l >> b THEN q1 ELSE q2 FI)
  | IQS_while : ∀ l b p q, is_quotientR_prog p q →
      is_quotientR_stmt (WHILE << l >> b DO p END)
                        (WHILE << l >> b DO q END)
  | IQS_assert : ∀ l b l', is_quotientR_stmt (ASSERT << l >> b =>> l')
                                                  (ASSERT << l >> b =>> l').

Scheme is_quotientR_prog_mutual_ind := Induction for is_quotientR_prog Sort Prop
  with is_quotientR_stmt_mutual_ind := Induction for is_quotientR_stmt Sort Prop.

Tactic Notation "is_quotientR_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "IQP_nil" | Case_aux c "IQP_remove" | Case_aux c "IQP_stmt"
  | Case_aux c "IQS_skip" | Case_aux c "IQS_ass" | Case_aux c "IQS_ifb"
  | Case_aux c "IQS_while" | Case_aux c "IQS_assert" ].

Theorem is_quotientR_refl : ∀ p,
  is_quotientR_prog p p.
Proof.
  intros p.
  prog_cases (apply (prog_mutual_ind
    (fun p ⇒ is_quotientR_prog p p)
    (fun s ⇒ is_quotientR_stmt s s))) Case; intros;
  try (constructor; fail).
  - Case "P_cons". apply IQP_stmt; assumption.
  - Case "S_ifb". apply IQS_ifb; assumption.
  - Case "S_while". apply IQS_while; assumption.
Qed.

Lemma is_quotientR_prog_num_lab : ∀ p q,
  is_quotientR_prog p q → num_lab_prog q ≤ num_lab_prog p.
Proof.
  is_quotientR_cases (apply (is_quotientR_prog_mutual_ind
    (fun p q H ⇒ num_lab_prog q ≤ num_lab_prog p)
    (fun s t H ⇒ num_lab_stmt t ≤ num_lab_stmt s))) Case; intros;
  simpl; omega.
Qed.

Lemma is_quotientR_stmt_num_lab : ∀ p q,
  is_quotientR_stmt p q → num_lab_stmt q ≤ num_lab_stmt p.
Proof.
  is_quotientR_cases (apply (is_quotientR_stmt_mutual_ind
    (fun p q H ⇒ num_lab_prog q ≤ num_lab_prog p)
    (fun s t H ⇒ num_lab_stmt t ≤ num_lab_stmt s))) Case; intros;
  simpl; omega.
Qed.

Theorem is_quotientR_prog_same_num : ∀ p q,
  is_quotientR_prog p q → num_lab_prog p = num_lab_prog q →
  p = q.
Proof.
  apply (is_quotientR_prog_mutual_ind
    (fun p q H ⇒ num_lab_prog p = num_lab_prog q → p = q)
    (fun s t H ⇒ num_lab_stmt s = num_lab_stmt t → s = t)); intros.
  subst.
  reflexivity.
  apply is_quotientR_prog_num_lab in i. simpl in H0.
  assert (num_lab_stmt s > 0) by (apply num_lab_stmt_lt). omega.
  apply is_quotientR_prog_num_lab in i.
  apply is_quotientR_stmt_num_lab in i0.
  simpl in H1. assert (num_lab_stmt s = num_lab_stmt s'). omega.
  assert (num_lab_prog p = num_lab_prog q). omega. intuition. subst. reflexivity.
  reflexivity. reflexivity.
  simpl in H1. apply is_quotientR_prog_num_lab in i.
  apply is_quotientR_prog_num_lab in i0.
  assert (num_lab_prog p1 = num_lab_prog q1). omega.
  assert (num_lab_prog p2 = num_lab_prog q2). omega.
  intuition; subst; reflexivity. simpl in H0. inversion H0.
  apply H in H2. subst; reflexivity.
  reflexivity.
Qed.

Theorem is_quotientR_antisym : ∀ p q,
  is_quotientR_prog p q → is_quotientR_prog q p → p = q.
Proof.
  intros.
  apply is_quotientR_prog_same_num.
  - assumption.
  - apply is_quotientR_prog_num_lab in H.
  apply is_quotientR_prog_num_lab in H0. omega.
Qed.

Theorem is_quotientR_trans : ∀ p q r,
  is_quotientR_prog p q → is_quotientR_prog q r → is_quotientR_prog p r.
Proof.
  intros p q r H.
  generalize dependent r. generalize dependent q.
  generalize dependent p.
  apply (is_quotientR_prog_mutual_ind
    (fun p q H ⇒ ∀ r, is_quotientR_prog q r → is_quotientR_prog p r)
    (fun s t H ⇒ ∀ u, is_quotientR_stmt t u → is_quotientR_stmt s u)); intros.
  assumption.
  constructor. apply H. assumption.
  inversion H1; subst. constructor. apply H. assumption.
  apply IQP_stmt. apply H. assumption.
  apply H0. assumption.
  assumption.
  assumption.
  inversion H1; subst. constructor. apply H. assumption.
  apply H0. assumption.
  inversion H0; subst. constructor. apply H. assumption.
  assumption.
Qed.

Theorem is_quotientR_in_seq : ∀ p p' q q',
  is_quotientR_prog p p' → is_quotientR_prog q q' → is_quotientR_prog (p+;+q) (p'+;+q').
Proof.
  intros. induction H.
  simpl. assumption.
  simpl. constructor. assumption.
  simpl. apply IQP_stmt; assumption.
Qed.

Theorem is_quotientR_prog_single : ∀ s s',
  is_quotientR_stmt s s' ↔ is_quotientR_prog {{s}} {{s'}}.
Proof.
  split.
  Case "->". intros. apply IQP_stmt. constructor. assumption.
  Case "<-". intros. inversion H. inversion H3. assumption.
Qed.