Library Congruence

Require Export Omega Coq.Setoids.Setoid List Util AutoIndTac Base Unfolding.

Set Implicit Arguments.
Unset Printing Records.

Require Import Autosubst.

Congruence for recursion

Lemma congruent_Fix_help s t n xi
  : s =T t → TC (unfold s n) xi → TC (CFPFix t) xi.
Proof.
  intros. general induction n.
  - simpl in H0. rewrite Null_trace; eauto using TC.
  - simpl in H0. constructor.
    assert (TC s.[CFPFix t /] xi).
    { apply subst_subsumption_transfer with (sigma1:= unfold s n.: ids); eauto.
      intros. destruct x.
      - asimpl. asimpl in H0. apply IHn with (s:= s); eauto.
      - asimpl. asimpl in H0. eauto. }
    apply subst_tracesubsumption_preserve with (s:= s).
    + intros. apply H. eauto.
    + eauto.
Qed.

Lemma congruent_Fix s t
  : s =T t → (CFPFix s ) =T (CFPFix t ).
Proof.
  intros. split; intros.
  + apply Fix_unfold_subsume in H0. destruct H0 as [n A].
    apply congruent_Fix_help with (s:= s) (n:= n); eauto.
  + apply Fix_unfold_subsume in H0. destruct H0 as [n A].
    apply congruent_Fix_help with (s:= t) (n:= n); eauto.
    symmetry in H. eauto.
Qed.

Congruence for sequential composition and choice

Lemma congruent_Seq s t u v
  : s =T u → t =T v → CFPSeq s t =T CFPSeq u v.
Proof.
  intros. split; intros.
  - inv H1; eauto using TC.
    constructor.
    + apply H. eauto.
    + apply H0. eauto.
  - inv H1; eauto using TC.
    constructor.
    + apply H. eauto.
    + apply H0. eauto.
Qed.

Lemma congruent_Choice s t u v
  : s =T u → t =T v → CFPChoice s t =T CFPChoice u v.
Proof.
  intros. split; intros.
  - inv H1; eauto using TC.
    + constructor. apply H. eauto.
    + constructor 7. apply H0. eauto.
  - inv H1; eauto using TC.
    + constructor. apply H. eauto.
    + constructor 7. apply H0. eauto.
Qed.

Registration of program equivalence as congruence relation for rewriting

Instance Seq_eqTC_proper:
  Proper (eqTC ==> eqTC ==> eqTC) (CFPSeq).
Proof.
  hnf. intros s1 s2. intros.
  hnf. intros t1 t2. intros.
  apply congruent_Seq; eauto.
Qed.

Instance Choice_eqTC_proper:
  Proper (eqTC ==> eqTC ==> eqTC) (CFPChoice).
Proof.
  hnf. intros s1 s2. intros.
  hnf. intros t1 t2. intros.
  apply congruent_Choice; eauto.
Qed.

Instance Fix_eqTC_proper:
  Proper (eqTC ==> eqTC) (CFPFix).
Proof.
  hnf. intros s t. intros.
  apply congruent_Fix; eauto.
Qed.