text:
(**
CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.

- Frederic Blanqui, 2005-02-17
- Adam Koprowski and Hans Zantema, 2007-03
- Joerg Endrullis and Dimitri Hendriks, 2008-07

General definitions and results about relations.
*)

Set Implicit Arguments.

From Coq Require Import Setoid Basics Morphisms List Omega.
From Coq Require Export Relations.
From Coq Require Import Lia.

From CoLoR Require Import LogicUtil.
From CoLoR Require Export RelMidex.

Arguments inclusion {A} R1 R2.
Arguments same_relation {A} R1 R2.
Arguments transp {A} R x y.
Arguments clos_refl_trans {A} R x y.
Arguments clos_trans {A} R x y.
Arguments reflexive {A} R.
Arguments transitive {A} R.
Arguments antisymmetric {A} R.
Arguments symmetric {A} R.
Arguments equiv {A} R.
Arguments union {A} R1 R2 x y.
Arguments lexprod [A B] _ _ _ _.
Arguments symprod [A B] _ _ _ _.

(***********************************************************************)
(** Notations for some relations and operations on relations. *)

Notation rel := relation.

Notation incl := inclusion.
Infix "<<" := incl (at level 50) : relation_scope.

Notation same := same_relation.
Infix "==" := same (at level 70).

Infix "U" := union (at level 45) : relation_scope.
Notation "x #" := (clos_refl_trans x) (at level 35) : relation_scope.
Notation "x !" := (clos_trans x) (at level 35) : relation_scope.

Open Scope relation_scope.

(***********************************************************************)
(** Properties of [incl]. *)

Instance incl_refl A : Reflexive (@incl A).

Proof. fo. Qed.

Ltac incl_refl := apply incl_refl.

Instance incl_trans A : Transitive (@incl A).

Proof. fo. Qed.

Ltac incl_trans S := apply incl_trans with S; try incl_refl.

Instance incl_same A : Proper (same ==> same ==> impl) (@incl A).

Proof. fo. Qed.

(*FIXME: try to remove*)
Lemma incl_elim A (R S : rel A) : R << S -> forall x y, R x y -> S x y.

Proof. auto. Qed.

Arguments incl_elim [A R S] _ [x y] _.

(***********************************************************************)
(** Properties of [same]. *)

Lemma rel_eq A (R S : rel A) : R == S <-> forall x y, R x y <-> S x y.

Proof. fo. Qed.

Instance same_equiv A : Equivalence (@same A).

Proof. fo. Qed.

(***********************************************************************)
(** Basic meta-theorems. *)

Lemma eq_incl_refl_rel A (R : rel A) : Reflexive R -> eq << R.

Proof. intros hR x y xy. subst y. apply hR. Qed.

Lemma sym A (R : rel A) x y : Symmetric R -> (R x y <-> R y x).

Proof. split_all. Qed.

(***********************************************************************)
(** Morphisms wrt [incl] and [same]. *)

Instance refl_same A : Proper (same ==> impl) (@Reflexive A).

Proof. fo. Qed.

Instance sym_same A : Proper (same ==> impl) (@Symmetric A).

Proof. fo. Qed.

Instance trans_same A : Proper (same ==> impl) (@Transitive A).

Proof.
  intros R S e h x y z xy yz. rewrite rel_eq in e. rewrite <- e in *.
  apply h with y; hyp.
Qed.

Instance equiv_same A : Proper (same ==> impl) (@Equivalence A).

Proof. intros R S RS [hr hs ht]. constructor; rewrite <- RS; hyp. Qed.

(***********************************************************************)
(** Properties of [Proper]. *)

Lemma prop2_incl A B C (f : A -> B -> C) :
  Proper (incl --> incl --> incl ==> impl)
         (fun R S T => Proper (R ==> S ==> T) f).

Proof.
  intros R R' RR' S S' SS' T T' TT' hf x x' xx' y y' yy'.
  apply TT'. apply hf; fo.
Qed.

Lemma prop3_incl A B C D (f : A -> B -> C -> D) :
  Proper (incl --> incl --> incl --> incl ==> impl)
         (fun R S T V => Proper (R ==> S ==> T ==> V) f).

Proof.
  intros R R' RR' S S' SS' T T' TT' V V' VV' hf x x' xx' y y' yy' z z' zz'.
  apply VV'. apply hf; fo.
Qed.

Lemma prop4_incl A B C D E (f : A -> B -> C -> D -> E) :
  Proper (incl --> incl --> incl --> incl --> incl ==> impl)
         (fun R S T V W => Proper (R ==> S ==> T ==> V ==> W) f).

Proof.
  intros R R' RR' S S' SS' T T' TT' V V' VV' W W' WW'
         hf x x' xx' y y' yy' z z' zz' a a' aa'.
  apply WW'. apply hf; fo.
Qed.

Instance prop_rel_same A (E : rel A) :
  Proper (same ==> impl) (Proper (E ==> E ==> impl)).

Proof.
  intros R S [RS SR] h x x' xx' y y' yy' xy.
  apply RS. eapply h. apply xx'. apply yy'. apply SR. hyp.
Qed.

Lemma prop_subrel A (R S : rel A) :
  Equivalence S -> subrelation R S -> Proper (R ==> R ==> impl) S.

Proof.
  intros S_eq RS u u' uu' v v' vv' uv. apply RS in uu'. apply RS in vv'.
  rewrite <- uu', <- vv'. hyp.
Qed.

Lemma prop_rel_sym A B (f : A -> B -> Prop) R S :
  Symmetric R -> Symmetric S
  -> Proper (R ==> S ==> impl) f -> Proper (R ==> S ==> iff) f.

Proof.
  intros R_sym S_sym f_prop x x' xx' y y' yy'. split; intro h.
  eapply f_prop. apply xx'. apply yy'. hyp.
  eapply f_prop. sym. apply xx'. sym. apply yy'. hyp.
Qed.

Instance equiv_prop A (R : rel A) :
  Transitive R -> Symmetric R -> Proper (R ==> R ==> impl) R.

Proof. intros R_trans R_sym t t' tt' u u' uu' tu. trans t. hyp. trans u; hyp. Qed.

(***********************************************************************)
(** Empty relation. *)

Definition empty_rel {A} : rel A := fun x y => False.

(***********************************************************************)
(** Relation associated to a boolean function. *)

Definition rel_of_bool A (f : A->A->bool) : rel A :=
  fun x y => f x y = true.

(***********************************************************************)
(** Boolean function associated to a decidable relation. *)

Section bool_of_rel.

  Variables (A : Type) (R : rel A) (R_dec : rel_dec R).

  Definition bool_of_rel t u := if R_dec t u then true else false.

  Lemma bool_of_rel_true x y : bool_of_rel x y = true <-> R x y.

  Proof.
    unfold bool_of_rel. split; destruct (R_dec x y).
    auto. discr. refl. tauto.
  Qed.

  Lemma bool_of_rel_false x y : bool_of_rel x y = false <-> ~R x y.

  Proof.
    unfold bool_of_rel. split; destruct (R_dec x y).
    discr. auto. tauto. refl.
  Qed.

  Lemma bool_of_rel_refl x : Reflexive R -> bool_of_rel x x = true.

  Proof.
    intro R_refl. unfold bool_of_rel. destruct (R_dec x x). refl.
    exfalso. apply n. refl.
  Qed.

  Global Instance bool_of_rel_prop :
    Symmetric R -> Transitive R -> Proper (R ==> R ==> Logic.eq) bool_of_rel.

  Proof.
    intros R_sym R_trans x x' xx' y y' yy'. unfold bool_of_rel.
    destruct (R_dec x y); destruct (R_dec x' y'); try refl.
    exfalso. apply n. trans x. hyp. trans y; hyp.
    exfalso. apply n. trans x'. hyp. trans y'; hyp.
  Qed.

End bool_of_rel.

Arguments bool_of_rel_true {A R} _ {x y}.
Arguments bool_of_rel_false {A R} _ {x y}.

(***********************************************************************)
(** Definition of some properties on relations. *)

Definition classic_left_total A B (R : A -> B -> Prop) :=
  forall x, exists y, R x y.

Definition left_total A B (R : A -> B -> Prop) :=
  forall x, {y | R x y}.

Definition functional A B (R : A -> B -> Prop) :=
  forall x y z, R x y -> R x z -> y = z.

Definition finitely_branching A B (R : A -> B -> Prop) :=
  forall x, {l | forall y, R x y <-> In y l}.

Definition irreflexive A (R : rel A) := forall x, ~R x x.

Definition asymmetric A (R : rel A) := forall x y, R x y -> ~R y x.

(** Predicate saying that [f] is an infinite sequence of [R]-steps. *)
Definition IS A (R : rel A) f := forall i, R (f i) (f (S i)).

Definition EIS A (R : rel A) := exists f, IS R f.

Definition NT A (R : rel A) x := exists f, f 0 = x /\ IS R f.

(** Predicate saying that [f] and [g] describe an infinite sequence
  of R-steps modulo E: for all i, f(i) E g(i) R f(i+1). *)
Definition ISMod A (E R : rel A) (f g : nat -> A) :=
  forall i, E (f i) (g i) /\ R (g i) (f (S i)).

(* Called PreOrder in Coq. *)
Definition quasi_ordering A (R : rel A) := reflexive R /\ transitive R.

Definition ordering A (R : rel A) :=
  reflexive R /\ transitive R /\ antisymmetric R.

Definition strict_ordering A (R : rel A) := irreflexive R /\ transitive R.

(***********************************************************************)
(** Strict part. *)

Definition strict_part A (R : rel A) : rel A := fun x y => R x y /\ ~R y x.

(***********************************************************************)
(** Intersection. *)

Definition intersection A (R S : rel A) : rel A := fun x y => R x y /\ S x y.

Lemma intersection_dec A (R S : rel A) (Rdec : rel_dec R) (Sdec : rel_dec S) :
  rel_dec (intersection R S).

Proof.
  intros x y. unfold intersection. case (Rdec x y); case (Sdec x y); intuition.
Defined.

(***********************************************************************)
(** Finitely branching relations. *)

Section finitely_branching.

  Variables (A : Type) (R : rel A) (FB : finitely_branching R).

  Definition sons x := proj1_sig (FB x).

  Lemma in_sons_R : forall x y, In y (sons x) -> R x y.

  Proof. intros x y. exact (proj2 (proj2_sig (FB x) y)). Qed.

  Lemma R_in_sons : forall x y, R x y -> In y (sons x).

  Proof. intros x y. exact (proj1 (proj2_sig (FB x) y)). Qed.

End finitely_branching.

Arguments in_sons_R [A R] _ [x y] _.
Arguments R_in_sons [A R] _ [x y] _.

(***********************************************************************)
(** Equivalence relation associated to a PreOrder. *)

Definition inter_transp A (R : rel A) : rel A := fun x y => R x y /\ R y x.

(*COQ: declaring these Lemma's as Instance's creates problems in
FSetUtil and FGraph *)

Lemma inter_transp_refl A (R : rel A) :
  Reflexive R -> Reflexive (inter_transp R).

Proof. fo. Qed.

Lemma inter_transp_sym A (R : rel A) : Symmetric (inter_transp R).

Proof. fo. Qed.

Lemma inter_transp_trans A (R : rel A) :
  Transitive R -> Transitive (inter_transp R).

Proof. fo. Qed.

Lemma inter_transp_incl A (R : rel A) : inter_transp R << R.

Proof. fo. Qed.

(***********************************************************************)
(** Properties of [IS]. *)

Instance IS_incl A : Proper (incl ==> Logic.eq ==> impl) (@IS A).

Proof. intros R S RS f g fg h i. subst. fo. Qed.

Instance IS_same A : Proper (same ==> Logic.eq ==> impl) (@IS A).

Proof. intros R S RS f g fg h. subst. fo. Qed.

Instance EIS_same A : Proper (same ==> impl) (@EIS A).

Proof. intros R S RS h. destruct h as [f h]. exists f. rewrite <- RS. hyp. Qed.

Lemma NT_IS_elt A (R : rel A) f k : IS R f -> NT R (f k).

Proof. intro hf. exists (fun i => f (i+k)). fo. Qed.

Lemma red_NT A (R : rel A) t u : R t u -> NT R u -> NT R t.

Proof.
  intros tu [f [f0 hf]]. subst.
  exists (fun k => match k with 0 => t | S k' => f k' end).
  intuition. intro k. destruct k. hyp. apply hf.
Qed.

(***********************************************************************)
(** Properties of [irreflexive]. *)

Instance irreflexive_incl A : Proper (incl --> impl) (@irreflexive A).

Proof. fo. Qed.

(***********************************************************************)
(** Monotony. *)

Definition monotone A B (R : rel A) (S : rel B) f :=
  forall x y, R x y -> S (f x) (f y).

Lemma monotone_transp A B (R : rel A) (S : rel B) f :
  monotone R S f -> monotone (transp R) (transp S) f.

Proof. unfold monotone, transp. auto. Qed.

(***********************************************************************)
(** Composition. *)

Definition compose A (R S : rel A) : rel A :=
  fun x y => exists z, R x z /\ S z y.

Infix "@" := compose (at level 40) : relation_scope.

Instance compose_incl A : Proper (incl ==> incl ==> incl) (@compose A).

Proof. fo. Qed.

(*FIXME: try to remove*)
Ltac comp := apply compose_incl; try incl_refl.

Instance compose_same A : Proper (same ==> same ==> same) (@compose A).

Proof. fo. Qed.

Definition absorbs_right A (R S : rel A) := R @ S << R.

Definition absorbs_left A (R S : rel A) := S @ R << R.

Lemma comp_assoc A (R S T : rel A) : (R @ S) @ T << R @ (S @ T).

Proof.
  unfold incl. intros. do 4 destruct H. exists x1; split. hyp.
  exists x0; split; hyp.
Qed.

Lemma comp_assoc' A (R S T : rel A) : R @ (S @ T) << (R @ S) @ T.

Proof.
  unfold incl. intros. do 2 destruct H. do 2 destruct H0.
  exists x1; split. exists x0; split; hyp. exact H1.
Qed.

Ltac assoc :=
  match goal with
    | |- (?s @ ?t) @ ?u << _ => incl_trans (s @ (t @ u)); try apply comp_assoc
    | |- ?s @ (?t @ ?u) << _ => incl_trans ((s @ t) @ u); try apply comp_assoc'
    | |- _ << (?s @ ?t) @ ?u => incl_trans (s @ (t @ u)); try apply comp_assoc'
    | |- _ << ?s @ (?t @ ?u) => incl_trans ((s @ t) @ u); try apply comp_assoc
  end.

Lemma absorbs_left_rtc A (R S : rel A) : R @ S << S -> R# @ S << S.

Proof.
  intro. unfold incl, compose. intros. do 2 destruct H0.
  gen H1. clear H1. elim H0; intros; auto. apply H. exists y0. auto.
Qed.

Lemma absorbs_right_rtc A (R S : rel A) : S @ R << S -> S @ R# << S.

Proof. intros h t v [u [tu uv]]. induction uv; fo. Qed.

(***********************************************************************)
(** Properties of [union]. *)

Instance union_incl A : Proper (incl ==> incl ==> incl) (@union A).

Proof. fo. Qed.

(*FIXME: try to remove*)
Ltac union := apply union_incl; try incl_refl.

Instance union_same A : Proper (same ==> same ==> same) (@union A).

Proof. fo. Qed.

Lemma union_commut A (R S : rel A) : R U S == S U R.

Proof. fo. Qed.

Lemma union_assoc A (R S T : rel A) : (R U S) U T == R U (S U T).

Proof. fo. Qed.

Lemma comp_union_l A (R S T : rel A) : (R U S) @ T == (R @ T) U (S @ T).

Proof. fo. Qed.

Lemma comp_union_r A (R S T : rel A) : T @ (R U S) == (T @ R) U (T @ S).

Proof. fo. Qed.

Lemma union_empty_r A (R : rel A) : R U empty_rel == R.

Proof. fo. Qed.

Lemma union_empty_l A (R : rel A) : empty_rel U R == R.

Proof. fo. Qed.

Lemma incl_union_l A (R S T : rel A) : R << S -> R << S U T.

Proof. fo. Qed.

Lemma incl_union_r A (R S T : rel A) : R << T -> R << S U T.

Proof. fo. Qed.

Lemma union_incl_eq A (R R' S : rel A) : R U R' << S <-> R << S /\ R' << S.

Proof. fo. Qed.

(***********************************************************************)
(** Reflexive closure. *)

Definition clos_refl A (R : rel A) : rel A := eq U R.

Notation "x %" := (clos_refl x) (at level 35) : relation_scope.

Instance rc_incl A : Proper (incl ==> incl) (@clos_refl A).

Proof. fo. Qed.

Instance rc_same A : Proper (same ==> same) (@clos_refl A).

Proof. fo. Qed.

Instance rc_refl A (R : rel A) : Reflexive (R%).

Proof. fo. Qed.

Instance rc_trans A (R : rel A) : Transitive R -> Transitive (R%).

Proof.
  intro. unfold Transitive, clos_refl, union. intros. decomp H0. subst y. hyp.
  decomp H1. subst z. auto. right. apply H with (y := y); hyp.
Qed.

Lemma incl_rc A (R : rel A) : R << R%.

Proof. fo. Qed.

(***********************************************************************)
(** Compatibility closure. *)

Section comp_clos.

  Variables (A : Type) (E : rel A) (E_eq : Equivalence E).

  Inductive comp_clos (R : rel A) : rel A :=
  | comp_clos_intro u u' v v' : E u u' -> E v v' -> R u' v' -> comp_clos R u v.

  Lemma comp_clos_intro_refl (R : rel A) t u : R t u -> comp_clos R t u.

  Proof. intro tu. eapply comp_clos_intro. refl. refl. hyp. Qed.

  Lemma comp_clos_eq R : same (comp_clos R) (E @ (R @ E)).

  Proof.
    split.
    intros t u tu. inversion_clear tu; subst. ex u'. intuition. ex v'. intuition.
    intros t u [t' [tt' [u' [t'u' u'u]]]]. eapply comp_clos_intro.
    apply tt'. sym. apply u'u. hyp.
  Qed.

  Lemma incl_comp_clos R : R << comp_clos R.

  Proof.
    intros u v uv. apply comp_clos_intro with (u':=u) (v':=v).
    refl. refl. hyp.
  Qed.

  Global Instance comp_clos_incl : Proper (incl ==> incl) comp_clos.

  Proof.
    intros R S RS u v uv. inversion uv; subst.
    apply comp_clos_intro with (u':=u') (v':=v'); fo.
  Qed.

  Global Instance comp_clos_same : Proper (same ==> same) comp_clos.

  Proof. intros R S [RS SR]. split. rewrite RS. refl. rewrite SR. refl. Qed.

  Lemma comp_clos_union R S :
    same (comp_clos (R U S)) (comp_clos R U comp_clos S).

  Proof.
    split.
    (* << *)
    induction 1.
    destruct H1 as [h|h]; [left|right];
      (eapply comp_clos_intro; [apply H | apply H0 | hyp]).
    (* >> *)
    intros t u [h|h].
    eapply comp_clos_incl. apply incl_union_l. refl. hyp.
    eapply comp_clos_incl. apply incl_union_r. refl. hyp.
  Qed.

  Global Instance comp_clos_prop R : Proper (E ==> E ==> impl) (comp_clos R).

  Proof.
    intros u u' uu' v v' vv' h. inversion h; subst.
    eapply comp_clos_intro.
    trans u. hyp. apply H.
    trans v. hyp. apply H0.
    hyp.
  Qed.

End comp_clos.

(***********************************************************************)
(** Properties of [clos_trans]. *)

Instance tc_trans A (R : rel A) : Transitive (R!).

Proof. unfold Transitive. intros. apply t_trans with y; hyp. Qed.

Instance tc_incl A : Proper (incl ==> incl) (@clos_trans A).

Proof.
  intros R R' H t u H0. elim H0; intros.
  apply t_step. apply H. hyp. trans y; hyp.
Qed.

Instance tc_same A : Proper (same ==> same) (@clos_trans A).

Proof. intros R S [RS SR]. split; apply tc_incl; hyp. Qed.

Lemma incl_tc A (R S : rel A) : R << S -> R << S!.

Proof. intros. unfold incl. unfold incl in H. intros. apply H in H0. apply t_step. trivial.  Qed.

Lemma trans_tc_incl A (R : rel A) : Transitive R -> R! << R.

Proof.
  unfold transitive, incl. intros. induction H0. hyp.
  apply H with y; hyp.
Qed.

Lemma trans_comp_incl A (R : rel A) : Transitive R -> R @ R << R.

Proof. fo. Qed.

Lemma absorbs_left_tc A (R S : rel A) : R @ S << S -> R! @ S << S.

Proof.
  intro. unfold incl, compose. intros. do 2 destruct H0.
  gen H1. clear H1. elim H0; intros; auto. apply H. exists y0. auto.
Qed.

Lemma tc_absorbs_left A (R S : rel A) : R @ S << S -> R @ S! << S!.

Proof.
  intro. unfold incl. intros. do 2 destruct H0. generalize x0 y H1 H0.
  induction 1; intros. apply t_step. apply H. exists x1; split; hyp.
  trans y0; auto.
Qed.

Lemma trans_intro A (R : rel A) : R @ R << R <-> Transitive R.

Proof.
  split. unfold Transitive. intros. apply H. exists y. intuition.
  intros h x z [y [xy yz]]. apply (h _ _ _ xy yz).
Qed.

Lemma comp_tc_idem A (R : rel A) : R! @ R! << R!.

Proof.
  unfold incl. intros. do 2 destruct H. trans x0; hyp.
Qed.

Lemma tc_min A (R S : rel A) : R << S -> Transitive S -> R! << S.

Proof.
  intros RS Strans. intros x y. induction 1. apply RS. hyp. trans y; hyp.
Qed.

Lemma trans_tc A (R : rel A) : Transitive R -> R! == R.

Proof. intro t. split. apply tc_min. refl. hyp. apply incl_tc. refl. Qed.

Lemma tc_idem A (R : rel A) : R!! == R!.

Proof.
  split. intros x y. induction 1. hyp. trans y; hyp.
  apply incl_tc. refl.
Qed.

Lemma tc_eq A (R S : rel A) : S << R -> R << S! -> R! == S!.

Proof.
  intros SR RSt. split; apply tc_min. hyp. apply tc_trans.
  trans R. hyp. apply incl_tc. refl. apply tc_trans.
Qed.

Lemma tc_incl_trans A (R S : rel A) : Transitive S -> R << S -> R! << S.

Proof. intros S_trans RS. intros t u tu; revert t u tu. induction 1; fo. Qed.

Instance tc_prop A (E R : rel A) : Reflexive E ->
  Proper (E ==> E ==> impl) R -> Proper (E ==> E ==> impl) (R!).

Proof.
  intros E_refl RE x x' xx' y y' yy' xy. revert x y xy x' xx' y' yy'.
  induction 1; intros x' xx' y' yy'.
  apply t_step. eapply RE. apply xx'. apply yy'. hyp.
  trans y. apply IHxy1. hyp. refl. apply IHxy2. refl. hyp.
Qed.

Lemma tc_prop_iff A (R E : rel A) : Equivalence E
  -> Proper (E ==> E ==> iff) R -> Proper (E ==> E ==> iff) (clos_trans R).

Proof.
  intros E_eq R_prop. apply prop_rel_sym; class. apply tc_prop; class.
  intros x x' xx' y y' yy' xy. rewrite <- xx', <- yy'. hyp.
Qed.

Lemma tc_step_l A (R : rel A) x y :
  R! x y -> R x y \/ (exists2 z, R x z & R! z y).

Proof.
  compute; intro xy; induction xy.
  left; trivial.
  inversion IHxy1; inversion IHxy2; right; solve [eauto |
    inversion H; try inversion H0; exists x0;
    [trivial | constructor 2 with y; auto]].
Qed.

Lemma tc_step_r A (R : rel A) x y :
  R! x y -> R x y \/ (exists2 z, R! x z & R z y).

Proof.
  compute; intro xy; induction xy.
  left; trivial.
  inversion_clear IHxy1; inversion_clear IHxy2; right;
    solve [eauto | inversion H0; exists x0;
    [constructor 2 with y; auto | trivial]].
Qed.

Lemma tc_transp A (R : rel A) : transp (R!) == (transp R)!.

Proof.
  intros; split; compute.
  induction 1.
  constructor; trivial.
  constructor 2 with y; auto.
  induction 1.
  constructor; trivial.
  constructor 2 with y; auto.
Qed.

(***********************************************************************)
(** Symmetric closure of a relation. *)

Section clos_sym.

  Variable (A : Type) (R : rel A).

  Inductive clos_sym : rel A :=
  | s_step : forall x y, R x y -> clos_sym x y
  | s_sym : forall x y, clos_sym y x -> clos_sym x y.

  Global Instance sc_sym : Symmetric clos_sym.

  Proof. intros x y xy. apply s_sym. hyp. Qed.

End clos_sym.

(***********************************************************************)
(** Reflexive, transitive and symmetric closure of a relation. *)

Section clos_equiv.

  Variable (A : Type) (R : rel A).

  Inductive clos_equiv : rel A :=
  | e_step : forall x y, R x y -> clos_equiv x y
  | e_refl : forall x, clos_equiv x x
  | e_trans : forall x y z, clos_equiv x y -> clos_equiv y z -> clos_equiv x z
  | e_sym : forall x y, clos_equiv x y -> clos_equiv y x.

  Global Instance ec_equiv : Equivalence clos_equiv.

  Proof. exact (Build_Equivalence _ e_refl e_sym e_trans). Qed.

End clos_equiv.

Instance ec_incl A : Proper (incl ==> incl) (@clos_equiv A).

Proof.
  intros R S RS x y; revert x y; induction 1.
  apply e_step. fo. refl. trans y; fo. sym. fo.
Qed.

Lemma ec_min A (R S : rel A) : Equivalence S -> R << S -> clos_equiv R << S.

Proof.
  intros S_eq RS. intros u v; revert u v; induction 1.
  fo. refl. trans y; hyp. hyp.
Qed.

(***********************************************************************)
(** Properties of [clos_refl_trans]. *)

Instance rtc_refl A (R : rel A) : Reflexive (R#).

Proof. unfold Reflexive. apply rt_refl. Qed.

Instance rtc_trans A (R : rel A) : Transitive (R#).

Proof. unfold Transitive. intros. eapply rt_trans. apply H. hyp. Qed.

Instance rtc_incl A : Proper (incl ==> incl) (@clos_refl_trans A).

Proof.
  intro. unfold incl. intros. elim H0; intros.
  apply rt_step. apply H. hyp. refl. trans y1; hyp.
Qed.

Instance rtc_same A : Proper (same ==> same) (@clos_refl_trans A).

Proof. intros R S [RS SR]. split; apply rtc_incl; hyp. Qed.

Lemma incl_rtc A (R : rel A) : R << R#.

Proof. unfold inclusion. intros. Print clos_refl_trans. apply rt_step. trivial. Qed.

Lemma tc_incl_rtc A (R : rel A) : R! << R#.

Proof. induction 1. apply rt_step. hyp. trans y; hyp. Qed.

Lemma tc_split A (R : rel A) : R! << R @ R#.

Proof.
  unfold incl. induction 1. exists y. split. hyp. refl.
  destruct IHclos_trans1. destruct H1. exists x0. split. hyp.
  trans y. hyp. apply incl_elim with (R:=R!). apply tc_incl_rtc. hyp.
Qed.

Lemma rc_incl_rtc A (R : rel A) : R% << R#.

Proof.
  unfold incl, clos_refl. intros. destruct H.
  subst y. refl. apply rt_step. exact H.
Qed.

Lemma rtc_split A (R : rel A) : R# << eq U R!.

Proof.
  unfold incl, union. intros. elim H.
  intros. right. apply t_step. hyp.
  intro. left. refl.
  intros. destruct H1; destruct H3.
  left. trans y0; hyp.
  subst y0. right. hyp.
  subst y0. right. hyp.
  right. trans y0; hyp.
Qed.

Lemma rtc_split_eq A (R : rel A) : R# == eq U R!.

Proof.
  split. apply rtc_split. rewrite union_incl_eq. split.
  intros x y h. subst. refl. apply tc_incl_rtc.
Qed.

Lemma rtc_split2 A (R : rel A) : R# << eq U R @ R#.

Proof.
  unfold incl, union. intros. elim H; clear H x y; intros.
  right. exists y; split. exact H. refl. auto. destruct H0.
  subst y. destruct H2. auto. destruct H0. right. exists x0. auto.
  do 2 destruct H0. right. exists x0. split. exact H0.
  trans y; auto.
Qed.

Lemma tc_split_inv A (R : rel A) : R# @ R << R!.

Proof.
  intros x y RRxy. destruct RRxy as [z [Rxz Rzy]].
  destruct (rtc_split Rxz).
  rewrite H. intuition.
  constructor 2 with z. hyp.
  constructor 1. hyp.
Qed.

Lemma tc_merge A (R : rel A) : R @ R# << R!.

Proof.
  unfold incl. intros. destruct H. destruct H.
  ded (rtc_split H0). destruct H1; subst.
  apply t_step; hyp. trans x0. apply t_step. hyp. hyp.
Qed.

Lemma rtc_transp A (R : rel A) : transp (R#) << (transp R)#.

Proof.
  unfold incl. induction 1. apply rt_step. hyp. refl. trans y; hyp.
Qed.

Lemma incl_rtc_rtc A (R S : rel A) : R << S# -> R# << S#.

Proof. unfold incl. induction 2. apply H. hyp. refl. trans y; hyp. Qed.

Lemma comp_rtc_idem A (R : rel A) : R# @ R# << R#.

Proof. unfold incl. intros. do 2 destruct H. trans x0; hyp. Qed.

Lemma trans_rtc_incl A (R : rel A) : Reflexive R -> Transitive R -> R# << R.

Proof. intros R_refl R_trans x y. induction 1. hyp. refl. trans y; hyp. Qed.

Lemma rtc_invol A (R : rel A) : R # # == R #.

Proof.
  split. intros x y. induction 1. hyp. refl. trans y; hyp. apply incl_rtc.
Qed.

Lemma rtc_intro_seq A (R : rel A) f i : forall j, i <= j ->
  (forall k, i <= k < j -> R (f k) (f (1+k))) -> R# (f i) (f j).

Proof.
  cut (forall n, (forall k, i <= k < i + n -> R (f k) (f (1+k))) ->
    R# (f i) (f (n+i))).
  intros h j ij hij. assert (j = (j-i) + i). omega.
  rewrite H. apply h.
  intros k hk. apply hij. omega.
  induction n; intro h. refl. trans (f (n+i)).
  apply IHn. intros k hk. apply h. omega.
  apply rt_step. apply h. omega.
Qed.

Lemma rtc_min A (R S : rel A) : PreOrder S -> R << S -> R# << S.

Proof.
  intros S_PO RS. intros u v; revert u v; induction 1.
  fo. refl. trans y; hyp.
Qed.

Instance rtc_sym A (R : rel A) : Symmetric R -> Symmetric (R#).

Proof.
  intros R_sym x; revert x; induction 1.
  apply rt_step. hyp. refl. trans y; hyp.
Qed.

(***********************************************************************)
(** Quasi-ordering closure. *)

Section qo_clos.

  Variables (A : Type) (E : rel A) (E_eq : Equivalence E).

  Inductive qo_clos (R : rel A) : rel A :=
  | qo_step : R << qo_clos R
  | qo_refl : E << qo_clos R
  | qo_trans : Transitive (qo_clos R).

  Variable R : rel A.

  Global Instance qo_clos_preorder : PreOrder (qo_clos R).

  Proof. split. intro x. apply qo_refl. refl. apply qo_trans. Qed.

  Variable R_prop : Proper (E ==> E ==> impl) R.

  Global Instance qo_clos_prop : Proper (E ==> E ==> impl) (qo_clos R).

  Proof.
    intros x x' xx' y y' yy' h. revert x y h x' xx' y' yy'.
    induction 1; intros x' xx' y' yy'.
    apply qo_step. rewrite <- xx', <- yy'. hyp.
    apply qo_refl. rewrite <- xx', <- yy'. hyp.
    trans y. apply IHh1. hyp. refl. apply IHh2. refl. hyp.
  Qed.

  (*COQ: if removed, Coq fails in LComp*)
  Global Instance qo_clos_prop_iff : Proper (E ==> E ==> iff) (qo_clos R).

  Proof. apply prop_rel_sym; class. Qed.

  Lemma qo_clos_inv : forall t u,
      qo_clos R t u -> E t u \/ exists v, R t v /\ qo_clos R v u.

  Proof.
    induction 1.
    right. ex y. intuition. auto.
    destruct IHqo_clos1 as [h1|[a [i1 i2]]];
      destruct IHqo_clos2 as [h2|[b [j1 j2]]].
    left. trans y; hyp.
    right. ex b. rewrite h1. auto.
    right. ex a. rewrite <- h2. auto.
    right. ex a. intuition. trans b. trans y. hyp. apply qo_step. hyp. hyp.
  Qed.

End qo_clos.

(***********************************************************************)
(** Properties of [transp]. *)

Instance transp_incl A : Proper (incl ==> incl) (@transp A).

Proof. fo. Qed.

Instance transp_same A : Proper (same ==> same) (@transp A).

Proof. fo. Qed.

(*COQ: declaring these lemmas as Global Instance makes Coq loop
  later in some other files *)

Lemma transp_refl A (R : rel A) : Reflexive R -> Reflexive (transp R).

Proof. auto. Qed.

Lemma transp_trans A (R : rel A) : Transitive R -> Transitive (transp R).

Proof. fo. Qed.

Lemma transp_sym A (R : rel A) : Symmetric R -> Symmetric (transp R).

Proof. fo. Qed.

Lemma transp_invol A (R : rel A) : transp (transp R) == R.

Proof. fo. Qed.

Lemma transp_union A (R S : rel A) : transp (R U S) == transp R U transp S.

Proof. fo. Qed.

(***********************************************************************)
(** Relations between closures, union and composition. *)

Lemma rtc_comp_permut A (R S : rel A) : R# @ (R# @ S)# << (R# @ S)# @ R#.

Proof.
  unfold incl. intros. do 2 destruct H. ded (rtc_split2 H0). destruct H1.
  subst x0. exists x; split. refl. exact H.
  do 4 destruct H1. exists y; split. trans x1.
  apply rt_step. exists x2; split. trans x0; hyp.
  hyp. hyp. refl.
Qed.

Lemma rtc_union A (R S : rel A) : (R U S)# << (R# @ S)# @ R#.

Proof.
  unfold incl. intros. elim H; intros.
  (* step *)
  destruct H0. exists x0; split. refl. apply rt_step. exact H0.
  exists y0; split. apply rt_step. exists x0; split. refl. exact H0.
  refl.
  (* refl *)
  exists x0; split; refl.
  (* trans *)
  do 2 destruct H1. do 2 destruct H3.
  assert (h : ((R# @ S)# @ clos_refl_trans R) x1 x2).
  apply incl_elim with (R := (R# @ clos_refl_trans (R# @ S))).
  apply rtc_comp_permut. exists y0; split; hyp.
  destruct h. destruct H6. exists x3; split.
  trans x1; hyp. trans x2; hyp.
Qed.

Lemma rtc_comp A (R S : rel A) : R# @ S << S U R! @ S.

Proof.
  unfold incl. intros. do 2 destruct H. ded (rtc_split H). destruct H1.
  subst x0. left. exact H0. right. exists x0; split; hyp.
Qed.

Lemma union_fact A (R S : rel A) : R U R @ S << R @ S%.

Proof.
  unfold incl. intros. destruct H.
  exists y; split; unfold clos_refl, union; auto.
  do 2 destruct H. exists x0; split; unfold clos_refl, union; auto.
Qed.

Lemma union_fact2 A (R S : rel A) : R @ S U R << R @ S%.

Proof. incl_trans (R U R @ S). apply union_commut. apply union_fact. Qed.

Lemma incl_rc_rtc A (R S : rel A) : R << S! -> R% << S#.

Proof.
  intro. unfold incl. intros. destruct H0. subst y. refl.
  apply incl_elim with (R := S!). apply tc_incl_rtc. apply H. exact H0.
Qed.

Lemma incl_tc_rtc A (R S : rel A) : R << S# -> R! << S#.

Proof. intro. unfold incl. induction 1. apply H. hyp. trans y; hyp. Qed.

Lemma rtc_comp_modulo A (R S : rel A) : R# @ (R# @ S)! << (R# @ S)!.

Proof.
  unfold incl. intros. do 2 destruct H.
  ded (tc_split H0). do 2 destruct H1. do 2 destruct H1.
  ded (rtc_split H2). destruct H4. subst x1.
  apply t_step. exists x2. intuition. trans x0; hyp.
  trans x1. apply t_step. exists x2. intuition.
  trans x0; hyp. exact H4.
Qed.

Lemma tc_union A (R S : rel A) : (R U S)! << R! U (R# @ S)! @ R#.

Proof.
  unfold incl. induction 1. destruct H. left. apply t_step. exact H.
  right. exists y. intuition. apply t_step. exists x. intuition.
  destruct IHclos_trans1. destruct IHclos_trans2.
  left. trans y; hyp.
  right. do 2 destruct H2. exists x0. intuition.
  apply rtc_comp_modulo. exists y. intuition. apply tc_incl_rtc. exact H1.
  right. do 2 destruct H1. destruct IHclos_trans2. exists x0.
  intuition. trans y. exact H2. apply tc_incl_rtc. exact H3.
  do 2 destruct H3. exists x1. intuition. trans x0. exact H1.
  apply rtc_comp_modulo. exists y. intuition.
Qed.

(***********************************************************************)
(** Commutation properties. *)

Section commut.

  Variables (A : Type) (R S : rel A) (commut : R @ S << S @ R).

  Lemma commut_rtc : R# @ S << S @ R#.

  Proof.
    unfold incl. intros. do 2 destruct H. generalize x x0 H y H0.
    clear H0 y H x0 x. induction 1; intros.
    assert ((S @ R) x y0). apply commut. exists y. intuition.
    do 2 destruct H1. exists x0. intuition.
    exists y. intuition.
    ded (IHclos_refl_trans2 _ H1). do 2 destruct H2.
    ded (IHclos_refl_trans1 _ H2). do 2 destruct H4.
    exists x1. intuition. trans x0; hyp.
  Qed.

  Lemma commut_rtc_inv : R @ S# << S# @ R.

  Proof.
    unfold incl. intros. do 2 destruct H. generalize x0 y H0 x H.
    clear H x x0 H0 y. induction 1; intros.
    assert ((S @ R) x0 y). apply commut. exists x. intuition.
    do 2 destruct H1. exists x1. intuition.
    exists x0. intuition.
    ded (IHclos_refl_trans1 _ H). do 2 destruct H0.
    ded (IHclos_refl_trans2 _ H1). do 2 destruct H2.
    exists x2. intuition. apply rtc_trans with x1; hyp.
  Qed.

  Lemma commut_tc : R! @ S << S @ R!.

  Proof.
    intros x y H. destruct H as [z Hxy].
    destruct (tc_split (proj1 Hxy)) as [z' Hz'].
    assert (SE : (S @ R#) z' y). apply commut_rtc. exists z. intuition.
    destruct SE as [x' Rx'].
    assert (SRx : (S @ R) x x'). apply commut. exists z'. intuition.
    destruct SRx as [y' Sy']. exists y'. split. intuition.
    apply tc_merge. exists x'. intuition.
  Qed.

  Lemma commut_tc_inv : R @ S! << S! @ R.

  Proof.
    intros x y H. destruct H as [z Hxy].
    destruct (tc_split (proj2 Hxy)) as [z' Hz'].
    assert (SRx : (S @ R) x z'). apply commut. exists z. intuition.
    destruct SRx as [y' Sy'].
    assert (SE : (S# @ R) y' y). apply commut_rtc_inv. exists z'. intuition.
    destruct SE as [x' Sx']. exists x'. split; try intuition.
    apply tc_merge. exists y'. intuition.
  Qed.

  Lemma commut_comp T : R @ (S @ T) << (S @ R) @ T.

  Proof. rewrite comp_assoc', commut. refl. Qed.

  Lemma comp_incl_assoc T V : R @ S << T -> R @ (S @ V) << T @ V.

  Proof. intro h. rewrite comp_assoc', h. refl. Qed.

End commut.

(***********************************************************************)
(** Inverse image. *)

Section inverse_image.

  Variables (A B : Type) (R : rel B) (f : A->B).

  Definition Rof : rel A := fun a a' => R (f a) (f a').

  (*COQ: declaring these lemmas as Global Instance makes Coq loop
  later in some other files *)

  Lemma Rof_refl : Reflexive R -> Reflexive Rof.

  Proof. fo. Qed.

  Lemma Rof_trans : Transitive R -> Transitive Rof.

  Proof. fo. Qed.

  Lemma Rof_sym : Symmetric R -> Symmetric Rof.

  Proof. fo. Qed.

  Lemma Rof_preorder : PreOrder R -> PreOrder Rof.

  Proof. fo. Qed.

  Lemma Rof_equiv : Equivalence R -> Equivalence Rof.

  Proof. fo. Qed.

  Variable F : A -> B -> Prop.

  Definition RoF : rel A :=
    fun a a' => exists b', F a' b' /\ forall b, F a b -> R b b'.

End inverse_image.

Instance Rof_incl A B : Proper (incl ==> Logic.eq ==> incl) (@Rof A B).

Proof. intros R S RS f g fg. subst g. fo. Qed.

(***********************************************************************)
(** Alternative definition of the transitive closure, more convenient
for some inductive proofs. *)

Inductive clos_trans1 A (R : rel A) : rel A :=
| t1_step : forall x y, R x y -> clos_trans1 R x y
| t1_trans : forall x y z, R x y -> clos_trans1 R y z -> clos_trans1 R x z.

Notation "x !1" := (clos_trans1 x) (at level 35) : relation_scope.

Instance tc1_trans A (R : rel A) : Transitive (R!1).

Proof.
  induction 1; intro H1.
  exact (t1_trans x H H1).
  exact (t1_trans x H (IHclos_trans1 H1)).
Qed.

Lemma tc1_eq A (R : rel A) x y : R!1 x y <-> R! x y.

Proof.
  split; induction 1.
  apply t_step. hyp. trans y. apply t_step. hyp. hyp.
  apply t1_step. hyp. trans y; hyp.
Qed.

(***********************************************************************)
(** Alternative definition of the reflexive and transitive closure,
more convenient for some inductive proofs. *)

Inductive clos_refl_trans1 A (R : rel A) : rel A :=
| rt1_refl : forall x, clos_refl_trans1 R x x
| rt1_trans : forall x y z,
  R x y -> clos_refl_trans1 R y z -> clos_refl_trans1 R x z.

Notation "x #1" := (clos_refl_trans1 x) (at level 9) : relation_scope.

Instance rtc1_preorder A (R : rel A) : PreOrder (R#1).

Proof.
  split; intro x. apply rt1_refl.
  induction 1; intro H1. hyp.
  exact (rt1_trans x H (IHclos_refl_trans1 H1)).
Qed.

Lemma rtc1_eq A (R : rel A) x y : R#1 x y <-> R# x y.

Proof.
  split; induction 1.
  refl. trans y. apply rt_step. hyp. hyp.
  eapply rt1_trans. apply H. refl. refl. trans y; hyp.
Qed.

Lemma tc1_incl_rtc1 A (R : rel A) : R!1 << R#1.

Proof.
  induction 1.
  eapply rt1_trans. apply H. refl.
  eapply rt1_trans. apply H. hyp.
Qed.

Lemma rtc1_union A (R S : rel A) : (R U S)#1 << (S#1 @ R)#1 @ S#1.

Proof.
  intros x y xRSy. induction xRSy as [ | x y z xRSy yRSz].
  exists x. split; refl.
  destruct IHyRSz as [m [ym mz]].
  destruct ym as [m | m n o mn no].
  induction xRSy as [xRy | xSy].
  exists m. split; trivial. apply rt1_trans with m.
  exists x. split; trivial. refl. refl.
  exists x. split. refl. apply rt1_trans with m; trivial.
  exists o. split; trivial.
  induction xRSy as [xRy | xSy].
  apply rt1_trans with m.
  exists x. split. refl. hyp.
  apply rtc1_preorder with n; trivial.
  apply rt1_trans with n; trivial. refl.
  apply rt1_trans with n.
  destruct mn as [q [mq qn]]. exists q. split; trivial.
  apply rt1_trans with m; hyp. hyp.
Qed.

Lemma union_rel_rt1_left A (R S : rel A) : R#1 << (R U S)#1.

Proof.
  intros x y xRy. induction xRy. refl.
  apply rt1_trans with y. left. hyp. hyp.
Qed.

Lemma union_rel_rt1_right A (R S : rel A) : S#1 << (R U S)#1.

Proof.
  intros x y xRy. induction xRy. refl.
  apply rt1_trans with y. right. hyp. hyp.
Qed.

Lemma incl_rt1_union_union A (R S : rel A) : (R!1 U S!1)#1 << (R U S)#1.

Proof.
  intros x y xRy. induction xRy. refl.
  apply rtc1_preorder with y; trivial.
  destruct H.
  apply union_rel_rt1_left. apply tc1_incl_rtc1. hyp.
  apply union_rel_rt1_right. apply tc1_incl_rtc1. hyp.
Qed.

Lemma incl_union_rt1_union A (R S : rel A) : (R U S)#1 << (R!1 U S!1)#1.

Proof.
  intros x y xRy. induction xRy. refl.
  apply rtc1_preorder with y; trivial.
  destruct H.
  apply union_rel_rt1_left. apply rt1_trans with y.
  apply t1_step. hyp. refl.
  apply union_rel_rt1_right. apply rt1_trans with y.
  apply t1_step. hyp. refl.
Qed.

Lemma comm_s_rt1 A (R S : rel A) :
  S@(R!1) << (R!1)@(S!1) -> (S!1)@(R!1) << (R!1)@(S!1).

Proof.
  intros comm x y [z [H1 H2]].
  induction H1 as [x z H | x y' z H H0 IH].
  apply comm.
  exists z; split; hyp.
  assert (H1 := IH H2); clear IH H2.
  destruct H1 as [u [H2 H3]].
  assert ((R!1 @ S!1) x u).
  apply comm. exists y'; split; hyp.
  destruct H1 as [m [xRm mSu]].
  exists m; split. hyp.
  exact (tc1_trans mSu H3).
Qed.

Lemma comm_s_r A (R S : rel A) :
  S@R << (R!1)@(S#1) -> (R U S)#1 @ R @ (R U S)#1 << (R!1) @ (R U S)#1.

Proof.
  intros comm x y [z2 [[z1 [xRSz1 z1Rz2]] z2RSy]].
  induction xRSz1 as [ | m n z1 mRSn nRSz1 IH].
  exists z2. split. apply t1_step. hyp. hyp.
  (* m RUS n RUS# z1 R z2 RUS# y *)
  assert (((R!1) @ (R U S)#1) n y) as mRedy. apply IH. hyp.
  (* m RUS n R!1@RUS#1 y *)
  clear nRSz1 z1Rz2 z2RSy IH z1 z2.
  destruct mRedy as [o [nRo oRSy]].
  (* m RUS n R!1 o RUS#1 y *)
  induction mRSn.
  (* m R n *)
  exists o. split; auto. apply t1_trans with n; hyp.
  (* m S n *)
  destruct nRo as [o p oRp | o p q oRp pRq ];

  assert (((R!1)@(S#1)) m p) as mRedp. apply comm; exists o; split; hyp.
  destruct mRedp as [x [mRx xSp]].
  exists x. split. hyp.
  apply rtc1_preorder with p.
  apply union_rel_rt1_right. hyp. hyp.

  assert (((R!1)@(S#1)) m p) as mRedp. apply comm; exists o; split; hyp.
  destruct mRedp as [x [mRx xSp]].
  exists x. split. hyp. hyp.
  destruct mRedp as [n [mRn sSp]].
  exists n; split. hyp.
  apply rtc1_preorder with q.
  apply rtc1_preorder with p.
  apply union_rel_rt1_right. hyp.
  apply union_rel_rt1_left. apply tc1_incl_rtc1. hyp.
  hyp.
Qed.

(***********************************************************************)
(** Extension to [option A] of a relation on [A] so that it is
reflexive on [None]. *)

Section opt_r.

  Variables (A : Type) (R : rel A).

  Inductive opt_r : rel (option A) :=
  | opt_r_None : opt_r None None
  | opt_r_Some : forall a b, R a b -> opt_r (Some a) (Some b).

  Global Instance opt_r_refl : Reflexive R -> Reflexive opt_r.

  Proof. intros h [x|]. apply opt_r_Some. refl. apply opt_r_None. Qed.

  Global Instance opt_r_sym : Symmetric R -> Symmetric opt_r.

  Proof.
    intros h x y xy. inversion xy; subst. hyp. apply opt_r_Some. sym. hyp.
  Qed.

  Global Instance opt_r_trans : Transitive R -> Transitive opt_r.

  Proof.
    intros h x y z xy yz. inversion xy; inversion yz; subst; try discr.
    apply opt_r_None. inversion H3; subst. apply opt_r_Some. trans b; hyp.
  Qed.

  Global Instance Some_prop : Proper (R ==> opt_r) (@Some A).

  Proof. intros x y xy. apply opt_r_Some. hyp. Qed.

End opt_r.

(****************************************************************************)
(** Extension of a relation on [A] to [option A] so that it is
irreflexive on [None]. *)

Section opt.

  Variables (A : Type) (R : rel A).

  Inductive opt : rel (option A) :=
  | opt_intro : forall x y, R x y -> opt (Some x) (Some y).

  Global Instance opt_trans : Transitive R -> Transitive opt.

  Proof.
    intros R_trans x y z xy yz. inversion xy; inversion yz; clear xy yz; subst.
    inversion H3; clear H3; subst. apply opt_intro. trans y0; hyp.
  Qed.

  Global Instance opt_sym : Symmetric R -> Symmetric opt.

  Proof.
    intros R_sym x y xy. inversion xy; clear xy; subst. apply opt_intro. hyp.
  Qed.

  Global Instance opt_opt_r E : Proper (E ==> E ==> impl) R ->
    Proper (opt_r E ==> opt_r E ==> impl) opt.

  Proof.
    intros R_E x x' xx' y y' yy' xy.
    inversion xy; inversion xx'; inversion yy'; clear xy xx' yy'; subst;
      try discr. inversion H6; inversion H3; clear H6 H3; subst.
    apply opt_intro. eapply R_E. apply H2. apply H5. hyp.
  Qed.

  Lemma opt_absorbs_right_opt_r E : R @ E << R -> opt @ opt_r E << opt.

  Proof.
    intros RE x z [y [xy yz]].
    inversion xy; clear xy; subst. inversion yz; clear yz; subst.
    apply opt_intro. apply RE. exists y0. fo.
  Qed.

  Lemma opt_absorbs_left_opt_r E : E @ R << R -> opt_r E @ opt << opt.

  Proof.
    intros ER x z [y [xy yz]].
    inversion yz; clear yz; subst. inversion xy; clear xy; subst.
    apply opt_intro. apply ER. exists x0. fo.
  Qed.

End opt.

Instance opt_incl A : Proper (incl ==> incl) (@opt A).

Proof.
  intros R S RS x y xy. inversion xy; clear xy; subst. apply opt_intro. fo.
Qed.

Instance opt_prop A (E1 E2 R : rel A) :
  Proper (E1 ==> E2 ==> impl) R -> Proper (opt E1 ==> opt E2 ==> impl) (opt R).

Proof.
  intros h x x' xx' y y' yy' xy. inversion xx'; clear xx'; subst.
  inversion yy'; clear yy'; subst. inversion xy; clear xy; subst.
  apply opt_intro. eapply h. apply H. apply H0. hyp.
Qed.

Lemma opt_absorbs_right A (R E : rel A) :
  R @ E << R -> opt R @ opt E << opt R.

Proof.
  intros RE x z [y [xy yz]].
  inversion xy; clear xy; subst. inversion yz; clear yz; subst.
  apply opt_intro. apply RE. exists y0. fo.
Qed.

Lemma opt_absorbs_left A (R E : rel A) :
  E @ R << R -> opt E @ opt R << opt R.

Proof.
  intros ER x z [y [xy yz]].
  inversion yz; clear yz; subst. inversion xy; clear xy; subst.
  apply opt_intro. apply ER. exists x0. fo.
Qed.

(***********************************************************************)
(** Restriction of a relation to some set. *)

Section restrict.

  Variables (A : Type) (P : A -> Prop) (R : rel A).

  Definition restrict : rel A := fun x y => P x /\ R x y.

  Global Instance restrict_prop E :
    Proper (E ==> impl) P -> Proper (E ==> E ==> impl) R ->
    Proper (E ==> E ==> impl) restrict.

  Proof.
    intros PE RE x x' xx' y y' yy' [hxy xy]. split.
    rewrite <- xx'. hyp. eapply RE. apply xx'. apply yy'. hyp.
  Qed.

End restrict.

Lemma restrict_union A (P : A -> Prop) R S :
  restrict P (R U S) == restrict P R U restrict P S.

Proof. fo. Qed.

author: sorinica

repo: spike-prover

save_path: github-repos/coq/sorinica-spike-prover


text:
Require Import Coq.Classes.EquivDec.
Require Import Coq.Program.Program.
Require Import Coq.micromega.Lia.
Import List.ListNotations.

Require Import Leapfrog.FinType.
Require Import Leapfrog.P4automaton.
Require Import Leapfrog.Syntax.
Require Import Leapfrog.ConfRel.

Require Import Leapfrog.Utils.FunctionalFP.

Set Implicit Arguments.
Section ReachablePairs.

  (* State identifiers. *)
  Variable (St1: Type).
  Context `{St1_eq_dec: EquivDec.EqDec St1 eq}.
  Context `{St1_finite: @Finite St1 _ St1_eq_dec}.

  Variable (St2: Type).
  Context `{St2_eq_dec: EquivDec.EqDec St2 eq}.
  Context `{St2_finite: @Finite St2 _ St2_eq_dec}.

  Notation St := (St1 + St2)%type.

  (* Header identifiers. *)
  Variable (Hdr: Type).
  Context `{Hdr_eq_dec: EquivDec.EqDec Hdr eq}.
  Context `{Hdr_finite: @Finite Hdr _ Hdr_eq_dec}.
  Variable (Hdr_sz: Hdr -> nat).

  Variable (a: P4A.t St Hdr_sz).

  Notation conf := (configuration (P4A.interp a)).

  Definition state_pair : Type :=
    state_template a * state_template a.
  Global Program Instance state_pair_eq_dec: EquivDec.EqDec state_pair eq :=
    { equiv_dec x y :=
        if Sumbool.sumbool_and _ _ _ _
             (state_template_eq_dec (fst x) (fst y))
             (state_template_eq_dec (snd x) (snd y))
        then in_left
        else in_right }.
  Next Obligation.
    destruct x, y.
    simpl in *.
    congruence.
  Qed.
  Next Obligation.
    intuition.
  Qed.

  Definition state_pair_eqb (l: state_pair) (r: state_pair) : bool :=
    if l == r then true else false.

  Lemma state_pair_eqb_tru :
    forall l r, l = r <-> state_pair_eqb l r = true.
  Proof.
    unfold state_pair_eqb.
    intros.
    destruct (equiv_dec l r); [unfold "===" in e; split; auto|].
    split; intros H; exfalso; congruence.
  Qed.

  Definition state_pairs : Type :=
    list state_pair.

  Definition reads_left (s: state_pair) : nat:=
    let '(s1, s2) := s in
    let len1 := s1.(st_buf_len) in
    let len2 := s2.(st_buf_len) in
    match s1.(st_state), s2.(st_state) with
    | inl s1, inl s2 =>
      Nat.min (P4A.size a s1 - len1)
              (P4A.size a s2 - len2)
    | inl s1, inr _ =>
      (P4A.size a s1 - len1)
    | inr _, inl s2 =>
      (P4A.size a s2 - len2)
    | inr _, inr _ => 1
    end.

  Lemma reads_left_lower_bound (q1 q2: conf):
    1 <= reads_left
        (conf_to_state_template q1,
         conf_to_state_template q2).
  Proof.
    unfold reads_left, configuration_room_left; simpl.
    pose proof (conf_buf_sane q1).
    pose proof (conf_buf_sane q2).
    destruct (conf_state q1), (conf_state q2);
    autorewrite with size' in *; simpl in *;
    Lia.lia.
  Qed.

  Lemma reads_left_commutative (t1 t2: state_template a):
    reads_left (t1, t2) = reads_left (t2, t1).
  Proof.
    unfold reads_left.
    destruct (st_state t1), (st_state t2); Lia.lia.
  Qed.

  Lemma reads_left_upper_bound (q1 q2: conf) (s: St):
    conf_state q1 = inl s ->
    reads_left
        (conf_to_state_template q1,
         conf_to_state_template q2) <= configuration_room_left q1.
  Proof.
    intros; unfold reads_left, configuration_room_left; simpl.
    rewrite H; autorewrite with size'; simpl.
    destruct (conf_state q2); Lia.lia.
  Qed.

  Definition advance (steps: nat) (t1: state_template a) (s: P4A.state_ref St) :=
    match s with
    | inl s =>
      let st := P4A.t_states a s in
      if Compare_dec.le_gt_dec (size a s) (t1.(st_buf_len) + steps)
      then List.map (fun r => {| st_state := r; st_buf_len := 0 |}) (possible_next_states _ _ _ st)
      else [{| st_state := t1.(st_state); st_buf_len := t1.(st_buf_len) + steps |}]
    | inr b => [{| st_state := inr false; st_buf_len := 0 |}]
    end.

  Lemma advance_correct_active q bs s:
    conf_state (a := interp a) q = inl s ->
    1 <= length bs <= configuration_room_left q ->
    List.In (conf_to_state_template (follow q bs))
      (advance (length bs)
        (conf_to_state_template q)
        (st_state (conf_to_state_template q))).
  Proof.
    intros.
    unfold configuration_room_left in H0.
    unfold advance; simpl; rewrite H in *.
    autorewrite with size' in H0; simpl in H0.
    destruct (Compare_dec.le_gt_dec _ _).
    - assert (P4A.size a s = conf_buf_len q + length bs) by Lia.lia.
      unfold conf_to_state_template.
      apply List.in_map_iff; eexists; split.
      + rewrite conf_buf_len_follow_transition; [reflexivity|].
        rewrite H; now autorewrite with size'.
      + simpl.
        apply conf_state_follow_transition_syntactic; auto.
        rewrite H.
        autorewrite with size'.
        simpl.
        lia.
    - left.
      unfold conf_to_state_template.
      f_equal.
      + rewrite conf_state_follow_fill; auto.
        rewrite H.
        now autorewrite with size'.
      + rewrite conf_buf_len_follow_fill; auto.
        rewrite H.
        now autorewrite with size'.
  Qed.

  Lemma advance_correct_passive q1 bs b:
    conf_state q1 = inr b ->
    1 <= length bs ->
    List.In (conf_to_state_template (follow q1 bs))
      (advance (length bs)
        (conf_to_state_template q1)
        (st_state (conf_to_state_template q1))).
  Proof.
    intros.
    destruct bs.
    - simpl in H0.
      Lia.lia.
    - autorewrite with follow.
      unfold advance; simpl.
      rewrite H.
      unfold conf_to_state_template.
      rewrite follow_done.
      + left.
        f_equal.
        erewrite conf_buf_len_done.
        reflexivity.
        rewrite follow_done.
        reflexivity.
        eapply conf_state_step_done.
        exact H.
      + now apply conf_state_step_done with (h := b).
  Qed.

  Lemma advance_correct q1 bs:
    (forall s, conf_state q1 = inl s ->
               length bs <= configuration_room_left q1) ->
    1 <= length bs ->
    List.In (conf_to_state_template (follow q1 bs))
      (advance (length bs)
        (conf_to_state_template q1)
        (st_state (conf_to_state_template q1))).
  Proof.
    intros.
    destruct (conf_state q1) eqn:?.
    - apply advance_correct_active with (s := s); intuition.
    - now apply advance_correct_passive with (b := b).
  Qed.

  Lemma interp_state_template_definite:
    forall q t,
      interp_state_template (a := a) t q ->
      conf_to_state_template q = t.
  Proof.
    intros.
    now apply interp_state_template_dichotomy with (c := q).
  Qed.

  Lemma advance_correct':
    forall prev1 prev2 succ1 c1 c2 bs,
      length bs = reads_left (prev1, prev2) ->
      interp_state_template prev1 c1 ->
      interp_state_template prev2 c2 ->
      interp_state_template succ1 (follow c1 bs) ->
      List.In succ1 (advance (reads_left (prev1, prev2))
                             prev1
                             (st_state prev1)).
  Proof.
    intros.
    rewrite <- H.
    rewrite
      <- interp_state_template_definite with (t := prev1) (q := c1),
      <- interp_state_template_definite with (t := succ1) (q := follow c1 bs)
      by auto.
    rewrite
      <- interp_state_template_definite with (t := prev1) (q := c1),
      <- interp_state_template_definite with (t := prev2) (q := c2)
      in H by auto.
    apply advance_correct; setoid_rewrite H.
    - intros.
      now apply reads_left_upper_bound with (s := s).
    - apply reads_left_lower_bound.
  Qed.

  Definition reachable_pair_step' (r0: state_pair) : nat * state_pairs :=
    let '(t1, t2) := r0 in
    let s1 := t1.(st_state) in
    let s2 := t2.(st_state) in
    let steps := reads_left r0 in
    (steps, List.list_prod (advance steps t1 s1)
                           (advance steps t2 s2)).

  Definition reaches (cur prev: state_template a * state_template a)
    : list (nat * (state_template a * state_template a)) :=
    let '(n, successors) := reachable_pair_step' prev in
    if List.In_dec (state_pair_eq_dec) cur successors
    then [(n, prev)]
    else [].

  Lemma reaches_prev:
    forall cur prev prev' size,
      List.In (size, prev') (reaches cur prev) ->
      prev' = prev.
  Proof.
    unfold reaches.
    intros.
    destruct (reachable_pair_step' _) in H.
    destruct (List.in_dec _ _) in H.
    - simpl in *; destruct H.
      + congruence.
      + tauto.
    - simpl in H; tauto.
  Qed.

  Lemma reachable_step_size:
    forall prev size s,
      reachable_pair_step' prev = (size, s) ->
      size = reads_left prev.
  Proof.
    unfold reachable_pair_step'.
    intros.
    destruct prev.
    congruence.
  Qed.

  Lemma reaches_length:
    forall size cur prev,
      List.In (size, prev) (reaches cur prev) ->
      size = reads_left prev.
  Proof.
    unfold reaches.
    intros.
    destruct (reachable_pair_step' _) eqn:?.
    destruct (List.in_dec _ _); simpl in *; [eauto with datatypes | tauto].
    destruct H; [|tauto].
    inversion H; subst.
    eapply reachable_step_size; eauto.
  Qed.

  Lemma reaches_exists:
    forall cur prev size l,
      reachable_pair_step' prev = (size, l) ->
      List.In cur l ->
      List.In (size, prev) (reaches cur prev).
  Proof.
    unfold reaches.
    intros.
    destruct (reachable_pair_step' _).
    inversion H; subst.
    destruct (List.in_dec _ _); [eauto with datatypes | tauto].
  Qed.

  Lemma follow_in_reaches:
    forall bs prev succ c1 c2,
      length bs = reads_left prev ->
      interp_state_template (fst prev) c1 ->
      interp_state_template (snd prev) c2 ->
      interp_state_template (fst succ) (follow c1 bs) ->
      interp_state_template (snd succ) (follow c2 bs) ->
      List.In (length bs, prev) (reaches succ prev).
  Proof.
    intros.
    unfold reaches.
    unfold reachable_pair_step'.
    destruct prev as (prev1, prev2).
    destruct succ as (succ1, succ2).
    simpl in H0, H1, H2, H3.
    destruct (List.in_dec state_pair_eq_dec _ _).
    - apply List.in_prod_iff in i; destruct i.
      left; now f_equal.
    - contradict n.
      apply List.in_prod_iff.
      split.
      + apply advance_correct' with (c1 := c1) (c2 := c2) (bs := bs); auto.
      + rewrite reads_left_commutative.
        apply advance_correct' with (c1 := c2) (c2 := c1) (bs := bs); auto.
        now rewrite reads_left_commutative.
  Qed.

  Definition reachable_pair_step (r0: state_pair) : state_pairs :=
    snd (reachable_pair_step' r0).

  Definition reachable_step (r: state_pairs) : state_pairs :=
    let r' := (List.concat (List.map reachable_pair_step r)) in
    List.nodup state_pair_eq_dec (r' ++ r).

  Fixpoint reachable_states' fuel r :=
    match fuel with
    | 0 => r
    | S fuel => reachable_step (reachable_states' fuel r)
    end.

  Lemma nodup_incl' {X: Type} {Heq: EqDec X eq}:
    forall (l1 l2: list X),
      List.incl l1 l2 <-> List.incl (List.nodup Heq l1) l2.
  Proof.
    split; intros.
    - induction l1; try easy.
      simpl.
      destruct (List.in_dec Heq a0 l1).
      + apply IHl1.
        apply List.incl_cons_inv in H.
        intuition.
      + apply List.incl_cons_inv in H.
        apply List.incl_cons; try easy.
        intuition.
    - induction l1; try easy.
      apply List.incl_cons.
      + apply H.
        simpl.
        destruct (List.in_dec Heq a0 l1).
        * now apply List.nodup_In.
        * now left.
      + apply IHl1.
        simpl in H.
        destruct (List.in_dec Heq a0 l1).
        * assumption.
        * apply List.incl_cons_inv in H.
          intuition.
  Qed.

  Lemma reachable_step_mono:
    forall r1 r2,
      List.incl r1 r2 ->
      List.incl (reachable_step r1) (reachable_step r2).
  Proof.
    intros.
    unfold reachable_step.
    rewrite List.nodup_incl.
    rewrite <- nodup_incl'.
    repeat rewrite <- List.flat_map_concat_map.
    apply List.incl_app.
    - apply List.incl_appl.
      intros ? ?.
      rewrite List.in_flat_map_Exists in *.
      now apply List.incl_Exists with (l1 := r1).
    - now apply List.incl_appr.
  Qed.

  Lemma reachable_states_mono:
    forall fuel r1 r2,
      List.incl r1 r2 ->
      List.incl (reachable_states' fuel r1)
                (reachable_states' fuel r2).
  Proof.
    induction fuel; intros.
    - simpl in *.
      now apply H.
    - simpl in *.
      apply reachable_step_mono.
      unfold reachable_step in *.
      now apply IHfuel.
  Qed.

  Lemma reachable_states_plus:
    forall f1 f2 r,
      reachable_states' (f1 + f2) r =
      reachable_states' f1 (reachable_states' f2 r).
  Proof.
    induction f1; intros.
    - rewrite plus_O_n.
      reflexivity.
    - replace (S f1 + f2) with (S (f1 + f2)) by lia.
      simpl.
      now rewrite IHf1.
  Qed.

  Lemma reachable_states_expansive:
    forall fuel r,
      List.incl r (reachable_states' fuel r).
  Proof.
    induction fuel; intros.
    - easy.
    - simpl.
      unfold reachable_step.
      rewrite List.nodup_incl.
      apply List.incl_appr.
      apply IHfuel.
  Qed.

  Lemma reachable_states_mono_fuel:
    forall f1 f2 r,
      f1 <= f2 ->
      List.incl (reachable_states' f1 r) (reachable_states' f2 r).
  Proof.
    intros.
    replace f2 with (f1 + (f2-f1)) by lia.
    rewrite reachable_states_plus.
    apply reachable_states_mono.
    apply reachable_states_expansive.
  Qed.

  Definition chain (l: list state_pair) :=
    forall l1 l2 p1 p2,
      l = l1 ++ [p1; p2] ++ l2 ->
      List.In p2 (reachable_pair_step p1).

  Lemma chain_split_left:
    forall l1 l2,
      chain (l1 ++ l2) ->
      chain l1.
  Proof.
    unfold chain.
    intros.
    apply (H l0 (l3 ++ l2)).
    repeat rewrite List.app_assoc.
    f_equal.
    now repeat rewrite <- List.app_assoc.
  Qed.

  Lemma chain_trivial:
    forall p, chain [p].
  Proof.
    unfold chain; intros.
    apply (f_equal (@List.length state_pair)) in H.
    repeat rewrite List.app_length in H.
    simpl in H.
    lia.
  Qed.

  Lemma chain_cons (p p': state_pair) (l: list state_pair):
    chain (l ++ [p]) ->
    List.In p' (reachable_pair_step p) ->
    chain (l ++ [p; p']).
  Proof.
    unfold chain in *; intros.
    destruct l2.
    - simpl in *.
      apply (f_equal (@List.rev state_pair)) in H1.
      repeat rewrite List.rev_app_distr in H1.
      simpl in H1.
      inversion H1.
      now subst.
    - apply (f_equal (@List.removelast state_pair)) in H1.
      replace [p; p'] with ([p] ++ [p']) in H1 by easy.
      rewrite List.app_assoc in H1.
      rewrite List.removelast_last in H1.
      rewrite List.app_assoc in H1.
      rewrite List.removelast_app in H1 by easy.
      apply (H l1 (List.removelast (s :: l2))).
      rewrite <- List.app_assoc in H1.
      exact H1.
  Qed.

  Lemma nodup_trivial {X: Type} (x: X):
    List.NoDup [x].
  Proof.
    constructor.
    - easy.
    - constructor.
  Qed.

  Lemma nodup_split_left {X: Type} (l1 l2: list X):
    List.NoDup (l1 ++ l2) ->
    List.NoDup l1.
  Proof.
    revert l2; induction l1; intros.
    - constructor.
    - inversion_clear H.
      constructor.
      + contradict H0.
        apply List.in_app_iff.
        now left.
      + now eapply IHl1 with (l2 := l2).
  Qed.

  Lemma reachability_sound fuel p r:
    List.In p (reachable_states' fuel r) ->
    exists lpre lpost s,
      List.In s r /\
      s :: lpost = lpre ++ [p] /\
      chain (s :: lpost) /\
      List.NoDup (s :: lpost).
  Proof.
    revert p r; induction fuel; intros.
    - simpl in H.
      exists nil, nil, p.
      simpl; repeat split; auto.
      + apply chain_trivial.
      + apply nodup_trivial.
    - simpl in H.
      unfold reachable_step in H.
      rewrite List.nodup_In, List.in_app_iff in H.
      destruct H; [|now apply IHfuel].
      rewrite <- List.flat_map_concat_map,
              List.in_flat_map_Exists,
              List.Exists_exists in H.
      destruct H as [p' [? ?]].
      apply IHfuel in H.
      destruct H as [lpre' [lpost' [s [? [? [? ?]]]]]].
      destruct (List.in_dec state_pair_eq_dec p ([s] ++ lpost')).
      + apply List.in_split in i.
        destruct i as [l1 [l2 ?]].
        exists l1.
        destruct l1.
        * exists nil, s.
          simpl in *.
          repeat split; auto.
          -- now inversion_clear H4.
          -- apply chain_trivial.
          -- apply nodup_trivial.
        * simpl in *.
          exists (l1 ++ [p]), s.
          repeat split; auto.
          -- now inversion_clear H4.
          -- rewrite H4 in H2.
             apply chain_split_left with (l2 := l2).
             inversion_clear H4.
             simpl.
             now rewrite <- List.app_assoc.
          -- rewrite H4 in H3.
             inversion_clear H4.
             eapply nodup_split_left with (l2 := l2).
             now rewrite <- List.app_comm_cons, <- List.app_assoc.
      + exists (lpre' ++ [p']), (lpost' ++ [p]), s.
        repeat split; auto.
        * rewrite List.app_comm_cons.
          now f_equal.
        * rewrite List.app_comm_cons, H1.
          rewrite <- List.app_assoc.
          apply chain_cons; auto.
          now rewrite <- H1.
        * rewrite List.app_comm_cons.
          apply NoDup_app; auto.
          -- apply nodup_trivial.
          -- intros.
             contradict n.
             inversion_clear n; try contradiction.
             now subst.
          -- intros.
             inversion_clear H4; try contradiction.
             now subst.
  Qed.

  Lemma reachability_complete':
    forall lpost lpre s p r,
      List.In s r ->
      s :: lpost = lpre ++ [p] ->
      chain (s :: lpost) ->
      List.In p (reachable_states' (length lpost) r).
  Proof.
    induction lpost using List.rev_ind; intros.
    - simpl.
      destruct lpre.
      + simpl in H1.
        inversion H0.
        now subst.
      + apply (f_equal (@List.length state_pair)) in H0.
        rewrite List.app_length in H0.
        simpl in H0.
        lia.
    - simpl.
      induction lpre using List.rev_ind.
      + simpl in H0.
        inversion H0.
        apply (f_equal (@List.rev state_pair)) in H4.
        simpl in H4.
        rewrite List.rev_unit in H4.
        discriminate.
      + rewrite List.app_length; simpl.
        replace (length lpost + 1) with (S (length lpost)) by lia; simpl.
        unfold reachable_step.
        rewrite List.nodup_In.
        rewrite List.in_app_iff.
        left.
        rewrite <- List.flat_map_concat_map.
        rewrite List.in_flat_map_Exists.
        rewrite List.Exists_exists.
        simpl in H0.
        exists x0.
        split.
        * eapply IHlpost with (s := s); auto.
          -- rewrite <- List.removelast_last with (a := x) at 1.
             rewrite <- List.removelast_last with (a := p).
             rewrite <- List.app_comm_cons.
             rewrite H0.
             reflexivity.
          -- unfold chain in *; intros.
             apply H1 with (l1 := l1) (l2 := l2 ++ [x]).
             rewrite List.app_comm_cons, H2.
             now repeat rewrite <- List.app_assoc.
        * rewrite H0 in H1.
          rewrite <- List.app_assoc in H1.
          simpl in H1.
          unfold chain in H1.
          apply H1 with (l1 := lpre) (l2 := nil).
          reflexivity.
  Qed.

  Lemma reachability_complete:
    forall lpost lpre s p r n,
      List.In s r ->
      s :: lpost = lpre ++ [p] ->
      chain (s :: lpost) ->
      length lpost <= n ->
      List.In p (reachable_states' n r).
  Proof.
    intros.
    apply reachable_states_mono_fuel with (f1 := length lpost); auto.
    now apply reachability_complete' with (s := s) (lpre := lpre).
  Qed.

  Definition valid_state_templates : list (state_template a) :=
    [{| st_state := inr false; st_buf_len := 0 |};
     {| st_state := inr true; st_buf_len := 0 |}] ++
    List.flat_map (fun s =>
      List.map (fun n => {| st_state := inl s; st_buf_len := n |})
               (List.seq 0 (size a s))
      ) (List.map inl (enum St1) ++ List.map inr (enum St2)).

  Definition valid_state_template (t: state_template a) :=
    match st_state t with
    | inr _ => st_buf_len t = 0
    | inl s => st_buf_len t < size a s
    end.

  Lemma valid_state_templates_accurate:
    forall t,
      valid_state_template t ->
      List.In t valid_state_templates.
  Proof.
    unfold valid_state_template; intros.
    destruct t.
    simpl in *.
    destruct st_state.
    - right; right.
      rewrite List.in_flat_map_Exists.
      rewrite List.Exists_exists.
      exists s.
      split.
      + rewrite List.in_app_iff.
        destruct s; [left | right];
        rewrite List.in_map_iff;
        exists s;
        split; auto;
        apply elem_of_enum.
      + rewrite List.in_map_iff.
        exists st_buf_len.
        split; auto.
        apply List.in_seq.
        lia.
    - destruct b; [right; left | left].
      all: now f_equal.
  Qed.

  Lemma valid_state_templates_closed:
    forall t,
      valid_state_template t ->
      (forall t' n,
        List.In t' (advance n t (st_state t)) ->
        valid_state_template t').
  Proof.
    unfold valid_state_template; intros.
    destruct (st_state t) eqn:?.
    - simpl in H0.
      destruct (Compare_dec.le_gt_dec _ _).
      + rewrite List.in_map_iff in H0.
        destruct H0 as [? [? ?]].
        rewrite <- H0; simpl.
        destruct x; auto.
        apply a.
      + destruct H0; try contradiction.
        rewrite <- H0.
        simpl.
        rewrite Heqs.
        unfold P4A.t_states in g.
        simpl in H0.
        simpl.
        lia.
   - destruct H0.
     + now rewrite <- H0.
     + contradiction.
  Qed.

  Definition valid_state_pair (p: state_pair) :=
    valid_state_template (fst p) /\ valid_state_template (snd p).

  Definition valid_state_pairs :=
    List.list_prod valid_state_templates valid_state_templates.

  Lemma valid_state_pairs_closed:
    forall p,
      valid_state_pair p ->
      (forall p',
        List.In p' (reachable_pair_step p) ->
        valid_state_pair p').
  Proof.
    unfold valid_state_pair in *; intros.
    unfold reachable_pair_step in H0.
    unfold reachable_pair_step' in H0.
    destruct p, p'.
    unfold snd in H0.
    apply List.in_prod_iff in H0.
    destruct H0.
    simpl in H; destruct H.
    simpl; split.
    - eapply valid_state_templates_closed with (t := s); auto.
      exact H0.
    - eapply valid_state_templates_closed with (t := s0); auto.
      exact H1.
  Qed.

  Lemma valid_state_pairs_accurate:
    forall p,
      valid_state_pair p ->
      List.In p valid_state_pairs.
  Proof.
    intros.
    destruct p.
    unfold valid_state_pairs.
    apply List.in_prod_iff.
    unfold valid_state_pair in H.
    simpl in H.
    split; now apply valid_state_templates_accurate.
  Qed.

  Lemma chain_preserve_valid:
    forall l p,
      valid_state_pair p ->
      chain (p :: l) ->
      forall p',
        List.In p' l ->
        valid_state_pair p'.
  Proof.
    induction l; intros.
    - contradiction.
    - assert (valid_state_pair a0).
      + apply (valid_state_pairs_closed H).
        now apply H0 with (l1 := nil) (l2 := l).
      + destruct H1.
        * subst; auto.
        * apply IHl with (p := a0); auto.
          unfold chain in *.
          intros.
          eapply H0 with (l1 := p :: l1) (l2 := l2).
          simpl.
          now f_equal.
  Qed.

  Lemma reachable_states_bound:
    forall fuel r,
      (forall p, List.In p r -> valid_state_pair p) ->
      List.incl (reachable_states' fuel r)
                (reachable_states' (length valid_state_pairs) r).
  Proof.
    intros.
    intros ? ?.
    apply reachability_sound in H0.
    destruct H0 as [lpre [lpost [s [? [? [? ?]]]]]].
    eapply reachability_complete with (s := s).
    - auto.
    - exact H1.
    - exact H2.
    - apply List.NoDup_incl_length; [now inversion H3 |].
      clear H1.
      induction lpost using List.rev_ind; intros; try easy.
      apply List.incl_app.
      + apply IHlpost.
        * now apply chain_split_left with (l2 := [x]).
        * now eapply nodup_split_left with (l2 := [x]).
      + unfold List.incl; intros.
        destruct H1; [subst | easy].
        apply valid_state_pairs_accurate.
        apply chain_preserve_valid with (p := s) (l := lpost ++ [a1]); auto.
        rewrite List.in_app_iff; right.
        apply List.in_eq.
  Qed.

  Lemma reachable_states_closed (r: list state_pair) (p1 p2: state_pair):
    (forall p, List.In p r -> valid_state_pair p) ->
    List.In p1 (reachable_states' (length valid_state_pairs) r) ->
    List.In p2 (reachable_step [p1]) ->
    List.In p2 (reachable_states' (length valid_state_pairs) r).
  Proof.
    intros.
    apply reachable_states_bound with (fuel := S (length valid_state_pairs)); auto.
    unfold reachable_states'.
    fold (reachable_states' (length valid_state_pairs) r).
    revert H1; apply reachable_step_mono.
    unfold List.incl; intros.
    destruct H1; try contradiction; now subst.
  Qed.

  Definition build_state_pair s1 s2 : state_pair :=
    ({| st_state := inl (inl s1); st_buf_len := 0 |},
      {| st_state := inl (inr s2); st_buf_len := 0 |}).

  Definition build_state_pairs s1 s2 : state_pairs :=
    [build_state_pair s1 s2].

  Definition reachable_states_fp := fp state_pairs reachable_step.
  Definition reachable_states_wit s1 s2 : state_pairs -> Type :=
    fp_wit _ reachable_step (build_state_pairs s1 s2).

  Definition reachable_states s1 s2 : state_pairs :=
    reachable_states' (length valid_state_pairs) (build_state_pairs s1 s2).

  Lemma reachable_iter_nodup:
    forall s1 s2 y,
      func_iter _ reachable_step (build_state_pairs s1 s2) y ->
      List.NoDup y.
  Proof.
    intros.
    eapply func_iter_rec' with (f := reachable_step) (a := build_state_pairs s1 s2); trivial.
    - eapply nodup_trivial.
    - intros.
      unfold reachable_step.
      eapply List.NoDup_nodup.
  Qed.

  Lemma nodup_cons:
    forall A (x: A) xs eq,
      List.nodup eq (x :: xs) =
      (if List.in_dec eq x xs then [] else [x]) ++ List.nodup eq xs.
  Proof.
    intros.
    unfold List.nodup.
    destruct (List.in_dec eq x xs) eqn:?.
    - exact eq_refl.
    - erewrite <- List.app_comm_cons.
      simpl.
      exact eq_refl.
  Qed.

  Lemma reachable_mono:
    forall ss,
    List.NoDup ss ->
      exists ss', reachable_step ss = ss' ++ ss.
  Proof.
    intros.
    unfold reachable_step.
    induction (List.concat (List.map reachable_pair_step ss)).
    - exists [].
      simpl.
      eapply List.nodup_fixed_point.
      trivial.
    - erewrite <- List.app_comm_cons.
      erewrite nodup_cons.
      destruct IHl.
      erewrite H0.
      exists ((if List.in_dec state_pair_eq_dec a0 (l ++ ss) then [] else [a0]) ++
      x).
      erewrite List.app_assoc.
      exact eq_refl.
  Qed.

  Lemma reachable_lvsp_fixedpoint:
    forall s1 s2,
      valid_state_pair (build_state_pair s1 s2) ->
      let fp := reachable_states' (length valid_state_pairs) (build_state_pairs s1 s2) in
      reachable_step fp = fp.
  Proof.
    intros.
    subst fp.
    eapply f_incl_fp.
    -
      intros.
      eapply reachable_mono.
      trivial.

    - intros. unfold reachable_step.
      eapply List.NoDup_nodup.
    - intros. unfold reachable_step.
      eapply List.NoDup_nodup.

    - intros.
      (* pose proof reachable_states_bound (S (length valid_state_pairs)). *)
      assert (
        (reachable_states' (S (length valid_state_pairs)) (build_state_pairs s1 s2)) =
        (reachable_step (reachable_states' (length valid_state_pairs) (build_state_pairs s1 s2)))
      ) by exact eq_refl.
      erewrite <- H0.
      eapply reachable_states_bound.
      simpl.
      intros.
      inversion H1.
      + subst p.
        trivial.
      + contradiction.
  Qed.

  Lemma reachable_lsvp_func_iter:
    forall s1 s2,
      func_iter _ reachable_step (build_state_pairs s1 s2) (reachable_states' (length valid_state_pairs) (build_state_pairs s1 s2)).
  Proof.
    intros.
    induction (length valid_state_pairs); [constructor|].
    unfold reachable_states'.
    fold reachable_states'.

    eapply func_iter_extend.
    - exact IHn.
    - constructor.
      constructor.
  Qed.

  Lemma reachable_lsvp_fp_wit:
    forall s1 s2,
      valid_state_pair (build_state_pair s1 s2) ->
      reachable_states_wit s1 s2 (reachable_states' (length valid_state_pairs) (build_state_pairs s1 s2)).
  Proof.
    intros.
    eapply func_iter_conv.
    - eapply reachable_lsvp_func_iter.
    - eapply reachable_lvsp_fixedpoint.
      trivial.
  Qed.

  Lemma reachable_states_wit_conv :
    forall s1 s2 ss,
      valid_state_pair (build_state_pair s1 s2) ->
      reachable_states_wit s1 s2 ss ->
      reachable_states s1 s2 = ss.
  Proof.
    intros.
    pose proof (reachable_lsvp_fp_wit H).
    unfold reachable_states.

    eapply fp_wit_converges.
    - exact X0.
    - exact X.
  Qed.

  Definition reachable_pair rs (q1 q2: conf) : Prop :=
    List.Exists (fun '(t1, t2) =>
                   interp_state_template t1 q1 /\
                   interp_state_template t2 q2)
                rs.

End ReachablePairs.

author: verified-network-toolchain

repo: leapfrog


text:
Require Import List.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt Le Gt.

Require Sorts PTS PTS_SigmaBool.
Module S := PTS.
Module T := PTS_SigmaBool.
Import T Sorts.withoutProp.

Reserved Notation "M 'ᵗ'" (at level 20).

Fixpoint tsl (t : S.Term) : T.Term :=
  match t with
  | S.Var v => Var v
  | S.Sort s => !s
  | S.Π A B => Σ (Π (A ᵗ) (B ᵗ)) Bool
  | S.λ A M => ⟨λ (A ᵗ) (M ᵗ), true⟩
  | S.App M N => (π1 (M ᵗ)) · (N ᵗ)
  | S.Eq A M N => Eq (A ᵗ) (M ᵗ) (N ᵗ)
  | S.refle M => refle (M ᵗ)
  | S.J A P t1 u t2 p => J (A ᵗ) (P ᵗ) (t1 ᵗ) (u ᵗ) (t2 ᵗ) (p ᵗ)
  end
where " M 'ᵗ'" := (tsl M).

Reserved Notation "Γ 'ᶜ'" (at level 50).

Fixpoint tsl_ctx (Γ : S.Env) : T.Env :=
  match Γ with
  | nil => nil
  | A :: Γ => (A ᵗ) :: (Γ ᶜ)
  end
where "Γ 'ᶜ'" := (tsl_ctx Γ).

Definition tsl_lift M : forall n k, (S.lift_rec n k M) ᵗ = (M ᵗ) ↑ n # k.
  induction M; cbn; intros; auto;
    try (now rewrite ?IHM, ?IHM1, ?IHM2, ?IHM3, ?IHM4, ?IHM5, ?IHM6).
  now destruct (le_gt_dec k v).
Defined.

Definition tsl_var_ctx Γ A v : S.item_lift A Γ v -> A ᵗ ↓ v ⊂ Γ ᶜ.
  induction 1 as [t [H1 H2]]. exists (t ᵗ). split. rewrite H1. apply tsl_lift.
  clear A H1. induction H2. econstructor. econstructor. exact IHitem.
Defined.
Hint Resolve tsl_var_ctx.

Definition tsl_subst M : forall N n, (S.subst_rec N M n) ᵗ = (M ᵗ)[n ← N ᵗ].
  induction M; cbn; intros; auto;
    try (now rewrite ?IHM, ?IHM1, ?IHM2, ?IHM3, ?IHM4, ?IHM5, ?IHM6).
  destruct (lt_eq_lt_dec v n); cbn.
  destruct s. reflexivity. apply tsl_lift. reflexivity.
Defined.

Tactic Notation "trans" := eapply Betas_trans; [eapply Betas_Beta|].

Definition tsl_red M N : S.Beta M N -> M ᵗ →→ N ᵗ.
  induction 1; cbn.
  rewrite tsl_subst. trans; eauto. eauto.
  all: induction IHBeta; eauto 3.
  all: econstructor; eauto.
Defined.
Hint Resolve tsl_red.

Definition tsl_conv M N : S.Betac M N -> M ᵗ ≡ N ᵗ.
  induction 1; eauto 2. constructor.
  induction H; eauto.
Defined.
Hint Resolve tsl_conv.

Lemma Bool_s Γ s : Γ ⊣ -> Γ ⊢ Bool : !s.
  intro. destruct s; now constructor.
Defined.
Hint Resolve Bool_s.

Definition tsl_correction :
  (forall Γ M A, S.typ Γ M A -> Γ ᶜ ⊢ M ᵗ : A ᵗ) /\ (forall Γ,  S.wf Γ -> Γ ᶜ ⊣).
Proof.
  unshelve eapply S.typ_induc; cbn; eauto 3.
  - intros Γ A B s s' s'' r _ H _ H0. destruct r.
    pose proof (cΠ (Rel0 _ _) H H0).
    simple refine (let X := cΣ H1 (cBool 0 _) in _). eauto.
    now rewrite PeanoNat.Nat.max_0_r in X.
  - intros Γ A B s s' s'' M r _ H _ H0 _ H1.
    econstructor. eauto.
    constructor. eapply wf_typ. eassumption.
  - intros Γ M N A B t H _ H0. rewrite tsl_subst. econstructor.
    econstructor. eassumption. assumption.
  - intros Γ A P t1 u t2 p s t H t0 H0 t3 H1. rewrite tsl_subst.
    rewrite tsl_subst in H0. econstructor; eassumption.
Defined.

(* Print Assumptions tsl_correction. *)

Definition tsl_consistency : (exists M, S.typ nil M S.empty) -> exists M', nil ⊢ M' : ⊥.
Proof.
  intros [M H]. apply tsl_correction in H. cbn in H.
  exists (π1 (M ᵗ)). eauto.
Defined.

author: CoqHott

repo: Program-translations-CC-omega


text:
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith.
Require Import bedrock2.ProgramLogic.
Require Import bedrock2.Semantics.
Require Import bedrock2.WeakestPrecondition.
Require Import bedrock2.WeakestPreconditionProperties.
Require Import coqutil.Word.Interface.
Require Import coqutil.Map.Interface.
Require Import coqutil.Tactics.Tactics.
Require Import Bedrock2Experiments.ProgramSemantics32.
Require Import Bedrock2Experiments.LibBase.AbsMMIO.
Require Import Bedrock2Experiments.StateMachineSemantics.
Require Import Bedrock2Experiments.StateMachineProperties.
Import Syntax.Coercions List.ListNotations.
Local Open Scope string_scope.

Section Proof.
  Context {word: word.word 32} {mem: map.map word Byte.byte}
          {word_ok: word.ok word} {mem_ok: map.ok mem}
          {M: state_machine.parameters}.
  (* Note that these two will have to be provided at proof linking time, not at straightline_call *)
  Context {M_ok: state_machine.ok M}
          (execution_unique: forall t s1 s2, execution t s1 -> execution t s2 -> s1 = s2).

  Global Instance spec_of_abs_mmio_write8 : spec_of "abs_mmio_write8" :=
    fun function_env =>
      forall (tr : trace) (m : mem) (s : M) (s' : M) (addr : word) (value : word) r,
        state_machine.reg_addr r = addr ->
        state_machine.write_step 1 s r value s' ->
        execution tr s ->
        call function_env abs_mmio_write8 tr m [addr; value]
        (fun tr' m' rets =>
          rets = []
          /\ tr' = ((map.empty, MMIOLabels.WRITE8, [addr; value], (map.empty, [])) :: tr)
          /\ execution tr' s'
          /\ m = m'
        ).
  Lemma abs_mmio_write8_correct :
    program_logic_goal_for_function! abs_mmio_write8.
  Proof.
    repeat straightline.
    eapply (interact_write 1); repeat straightline.
    - rewrite <- H. reflexivity.
    - do 2 eexists; ssplit; eauto.
    - rewrite <- H; ssplit; eauto.
      match goal with
      | H: execution ?t ?s1 |- execution ?t ?s2 =>
        replace s2 with s1;
        [exact H | eapply execution_unique]
      end.
      all: eapply execution_step_write; [..|eassumption]; eauto.
  Qed.

  Global Instance spec_of_abs_mmio_write32 : spec_of "abs_mmio_write32" :=
    fun function_env =>
      forall (tr : trace) (m : mem) (s : M) (s' : M) (addr : word) (value : word) r,
        state_machine.reg_addr r = addr ->
        state_machine.write_step 4 s r value s' ->
        execution tr s ->
        call function_env abs_mmio_write32 tr m [addr; value]
        (fun tr' m' rets =>
          rets = []
          /\ tr' = ((map.empty, MMIOLabels.WRITE32, [addr; value], (map.empty, [])) :: tr)
          /\ execution tr' s'
          /\ m = m'
        ).
  Lemma abs_mmio_write32_correct :
    program_logic_goal_for_function! abs_mmio_write32.
  Proof.
    repeat straightline.
    eapply (interact_write 4); repeat straightline.
    - rewrite <- H. reflexivity.
    - do 2 eexists; ssplit; eauto.
    - rewrite <- H; ssplit; eauto.
      match goal with
      | H: execution ?t ?s1 |- execution ?t ?s2 =>
        replace s2 with s1;
        [exact H | eapply execution_unique]
      end.
      all: eapply execution_step_write; [..|eassumption]; eauto.
  Qed.

  Global Instance spec_of_abs_mmio_read8 : spec_of "abs_mmio_read8" :=
    fun function_env =>
      forall (tr : trace) (m : mem) (s : M) (addr : word) r val s',
        state_machine.reg_addr r = addr ->
        state_machine.read_step 1 s r val s' ->
        execution tr s ->
        call function_env abs_mmio_read8 tr m [addr]
        (fun tr' m' rets =>
          exists s' val,
          rets = [val]
          /\ tr' = ((map.empty, MMIOLabels.READ8, [addr], (map.empty, [val])) :: tr)
          /\ state_machine.read_step 1 s r val s' (* <-- redundant, but convenient *)
          /\ execution tr' s'
          /\ m = m'
        ).
  Lemma abs_mmio_read8_correct :
    program_logic_goal_for_function! abs_mmio_read8.
  Proof.
    repeat straightline.
    eapply (interact_read 1); repeat straightline; eauto.
    - rewrite <- H. reflexivity.
    - match goal with
      | H1: execution ?t ?s1, H2: execution ?t ?s2 |- _ =>
        pose proof (execution_unique _ _ _ H1 H2);
        subst s2;
        clear H2
      end.
      do 3 eexists; ssplit; eauto.
      rewrite <- H. reflexivity.
  Qed.

  Global Instance spec_of_abs_mmio_read32 : spec_of "abs_mmio_read32" :=
    fun function_env =>
      forall (tr : trace) (m : mem) (s : M) (addr : word) r val s',
        state_machine.reg_addr r = addr ->
        state_machine.read_step 4 s r val s' ->
        execution tr s ->
        call function_env abs_mmio_read32 tr m [addr]
        (fun tr' m' rets =>
          exists s' val,
          rets = [val]
          /\ tr' = ((map.empty, MMIOLabels.READ32, [addr], (map.empty, [val])) :: tr)
          /\ state_machine.read_step 4 s r val s' (* <-- redundant, but convenient *)
          /\ execution tr' s'
          /\ m = m'
        ).
  Lemma abs_mmio_read32_correct :
    program_logic_goal_for_function! abs_mmio_read32.
  Proof.
    repeat straightline.
    eapply (interact_read 4); repeat straightline; eauto.
    - rewrite <- H. reflexivity.
    - match goal with
      | H1: execution ?t ?s1, H2: execution ?t ?s2 |- _ =>
        pose proof (execution_unique _ _ _ H1 H2);
        subst s2;
        clear H2
      end.
      do 3 eexists; ssplit; eauto.
      rewrite <- H. reflexivity.
  Qed.

End Proof.

author: project-oak

repo: silveroak

save_path: github-repos/coq/project-oak-silveroak


text:
(* Distributed under the terms of the MIT license. *)
From Coq Require Import ssreflect ssrbool.
From MetaCoq.Utils Require Import utils.
From MetaCoq.Common Require Import config uGraph EnvMap.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICEquality PCUICReduction
     PCUICReflect PCUICSafeLemmata PCUICTyping PCUICGlobalEnv PCUICWfUniverses.
From MetaCoq.SafeChecker Require Import PCUICEqualityDec PCUICWfEnv.
From Equations Require Import Equations.

Class abstract_guard_impl :=
  { guard_impl : FixCoFix -> global_env_ext -> context -> mfixpoint term -> bool ;
    guard_correct : forall fix_cofix Σ Γ mfix, guard fix_cofix Σ Γ mfix <-> guard_impl fix_cofix Σ Γ mfix
  }.

Definition fake_guard_impl : FixCoFix -> global_env_ext -> context -> mfixpoint term -> bool
  := fun fix_cofix Σ Γ mfix => true.

Record reference_impl_ext {cf:checker_flags} {guard : abstract_guard_impl} := {
      reference_impl_env_ext :> global_env_ext;
      reference_impl_ext_wf :> ∥ wf_ext reference_impl_env_ext ∥;
      reference_impl_ext_graph := projT1 (graph_of_wf_ext reference_impl_ext_wf);
      reference_impl_ext_graph_wf := projT2 (graph_of_wf_ext reference_impl_ext_wf)
  }.

Record reference_impl {cf:checker_flags} := {
      reference_impl_env :> global_env;
      reference_impl_wf :> ∥ wf reference_impl_env ∥;
      reference_impl_graph := projT1 (graph_of_wf reference_impl_wf);
      reference_impl_graph_wf := projT2 (graph_of_wf reference_impl_wf)
  }.

Program Definition reference_pop {cf:checker_flags} (Σ : reference_impl) : reference_impl :=
match Σ.(declarations) with
 [] => Σ
 | (d::decls) =>
   {| reference_impl_env := {| universes := Σ.(universes); declarations := decls; retroknowledge := Σ.(retroknowledge) |} |}
end.
Next Obligation.
destruct Σ.(reference_impl_wf). sq.
destruct X as [onu ond]; split => //. rewrite <- Heq_anonymous in ond.
now depelim ond.
Qed.

Program Definition make_wf_env_ext {cf:checker_flags} {guard : abstract_guard_impl}
(Σ : reference_impl) (univs : universes_decl)
(prf : forall Σ0 : global_env, Σ0 = Σ -> ∥ wf_ext (Σ0, univs) ∥) : reference_impl_ext :=
{| reference_impl_env_ext := (Σ, univs);|}.

Program Global Instance canonical_abstract_env_struct {cf:checker_flags} {guard : abstract_guard_impl} :
  abstract_env_struct reference_impl reference_impl_ext :=
  {|
  abstract_env_lookup := fun Σ => lookup_env (reference_impl_env_ext Σ) ;
  abstract_env_leqb_level_n := fun Σ => leqb_level_n (reference_impl_ext_graph Σ) ;
  abstract_env_level_mem := fun Σ l => LevelSet.mem l (global_ext_levels (reference_impl_env_ext Σ));
  abstract_env_guard := fun Σ fix_cofix => guard_impl fix_cofix (reference_impl_env_ext Σ);
  abstract_env_ext_rel := fun X Σ => Σ = reference_impl_env_ext X;
  abstract_env_init := fun cs retro H =>  {|
     reference_impl_env := {| universes := cs ;
                               declarations := [];
                               retroknowledge := retro |}; |} ;
  abstract_env_add_decl := fun X kn d H =>
    {| reference_impl_env := add_global_decl X.(reference_impl_env) (kn,d); |};
  abstract_env_is_consistent X uctx :=
   let G := reference_impl_graph X in
   let G' := add_uctx uctx G in
   wGraph.is_acyclic G' && wGraph.IsFullSubgraph.is_full_extension G G' ;
  abstract_env_add_udecl X udecl Hglobal :=
    {| reference_impl_env_ext := (X.(reference_impl_env) , udecl); |} ;
  abstract_primitive_constant := fun X tag => primitive_constant X tag;
  abstract_env_rel := fun X Σ => Σ = reference_impl_env X ;
  abstract_pop_decls := reference_pop ;
 |}.
Next Obligation. sq; constructor; cbn; eauto. econstructor. Qed.
Next Obligation.
 pose proof (reference_impl_wf X). destruct (H _ eq_refl).
 sq. destruct H0.  econstructor; eauto. econstructor; eauto.
  Qed.
Next Obligation.
  pose proof (reference_impl_wf X). destruct (Hglobal _ eq_refl); sq.
  now econstructor.
Qed.

(* We pack up all the information required on the global environment and graph in a
single record. *)

Record wf_env {cf:checker_flags} := {
  wf_env_reference :> reference_impl;
  wf_env_map :> EnvMap.t global_decl;
  wf_env_map_repr :> EnvMap.repr (reference_impl_env wf_env_reference).(declarations) wf_env_map;
}.

Record wf_env_ext {cf:checker_flags} {guard : abstract_guard_impl} := {
  wf_env_ext_reference :> reference_impl_ext;
  wf_env_ext_map :> EnvMap.t global_decl;
  wf_env_ext_map_repr :> EnvMap.repr (reference_impl_env_ext wf_env_ext_reference).(declarations) wf_env_ext_map;
}.

Lemma wf_env_eta {cf : checker_flags} (Σ : wf_env) :
 {| universes := Σ.(universes); declarations := Σ.(declarations); retroknowledge := Σ.(retroknowledge) |} = Σ.
Proof.
  destruct Σ => /= //. destruct reference_impl_env => //.
Qed.

Lemma wf_fresh_globals {cf : checker_flags} Σ : wf Σ -> EnvMap.fresh_globals Σ.(declarations).
Proof. destruct Σ as [univs Σ]; cbn.
  move=> [] onu; cbn. induction 1; constructor; auto. now destruct o.
Qed.

Lemma wf_env_fresh {cf : checker_flags} (Σ : wf_env) : EnvMap.EnvMap.fresh_globals Σ.(declarations).
Proof.
  destruct Σ.(reference_impl_wf).
  now eapply wf_fresh_globals.
Qed.

Lemma of_global_env_cons {cf:checker_flags} d g : EnvMap.fresh_globals (add_global_decl g d).(declarations) ->
  EnvMap.of_global_env (add_global_decl g d).(declarations) = EnvMap.add d.1 d.2 (EnvMap.of_global_env g.(declarations)).
Proof.
  unfold EnvMap.of_global_env. simpl. unfold KernameMapFact.uncurry.
  reflexivity.
Qed.

Program Definition wf_env_init {cf:checker_flags} {guard : abstract_guard_impl} cs retro :
  on_global_univs cs -> wf_env := fun H =>
  {|
  wf_env_reference := abstract_env_init cs retro H;
  wf_env_map := EnvMap.empty;
  |}.

Lemma reference_pop_decls_correct {cf:checker_flags} (X:reference_impl) decls
  (prf : forall Σ : global_env, Σ = X ->
  exists d, Σ.(declarations) = d :: decls) :
  let X' := reference_pop X in
  forall Σ Σ', Σ = X -> Σ' = X' ->
          Σ'.(declarations) = decls /\ Σ.(universes) = Σ'.(universes) /\
          Σ.(retroknowledge) = Σ'.(retroknowledge).
Proof.
  cbn; intros; subst. specialize (prf _ eq_refl).
  unfold reference_pop. cbn. set (reference_pop_obligation_1 cf X).
  clearbody s. destruct (X.(declarations)); cbn; inversion prf; now inversion H.
Qed.

Program Definition optim_pop {cf:checker_flags} (Σ : wf_env) : wf_env :=
  match Σ.(reference_impl_env).(declarations) with
    [] => Σ
    | ((kn , d) :: decls) =>
    {| wf_env_reference := reference_pop Σ ;
        wf_env_map := EnvMap.EnvMap.remove kn Σ.(wf_env_map);
    |}
  end.

Next Obligation.
  pose proof Σ.(wf_env_map_repr). red in H.
  rewrite <- Heq_anonymous in H.
  set (Σ0 := EnvMap.of_global_env decls).
  pose proof (EnvMap.remove_add_eq decls kn d Σ0).
  PCUICSR.forward_keep H0.
  { pose proof (Σf := wf_env_fresh Σ). rewrite <- Heq_anonymous in Σf. now depelim Σf. }
  PCUICSR.forward_keep H0.
  { pose proof (Σf := wf_env_fresh Σ). rewrite <- Heq_anonymous in Σf. now depelim Σf. }
  PCUICSR.forward_keep H0.
  { red. unfold EnvMap.equal. reflexivity. }
  unfold EnvMap.repr.
  rewrite H /=. unfold KernameMapFact.uncurry; cbn.
  unfold EnvMap.add in H0.
  unfold reference_pop. cbn. set (reference_pop_obligation_1 cf _).
  clearbody s.
  destruct (declarations Σ); cbn in *; inversion Heq_anonymous; clear Heq_anonymous s.
  subst. unfold KernameMapFact.uncurry in *; cbn in *.
  unfold Σ0 in * ; clear Σ0. unfold EnvMap.equal, KernameMap.Equal in H0.
  specialize (H0 y). cbn in H0. rewrite H0. reflexivity.
Qed.

Program Global Instance optimized_abstract_env_struct {cf:checker_flags} {guard : abstract_guard_impl} :
  abstract_env_struct wf_env wf_env_ext :=
 {|
 abstract_env_lookup := fun Σ k => EnvMap.lookup k (wf_env_ext_map Σ);
 abstract_env_leqb_level_n X := abstract_env_leqb_level_n X.(wf_env_ext_reference);
 abstract_env_level_mem X := abstract_env_level_mem X.(wf_env_ext_reference);
 abstract_env_guard := fun Σ fix_cofix => guard_impl fix_cofix (wf_env_ext_reference Σ);
 abstract_env_ext_rel X := abstract_env_ext_rel X.(wf_env_ext_reference);

 abstract_env_init := wf_env_init;
 abstract_env_add_decl X kn d H :=
  {| wf_env_reference := @abstract_env_add_decl _ _ reference_impl_ext _ X.(wf_env_reference) kn d H ;
     wf_env_map := EnvMap.add kn d X.(wf_env_map) |};
 abstract_env_is_consistent X uctx := abstract_env_is_consistent X.(wf_env_reference) uctx;
 abstract_env_add_udecl X udecl Hdecl :=
 {| wf_env_ext_reference := @abstract_env_add_udecl _ _ reference_impl_ext _ X.(wf_env_reference) udecl Hdecl ;
    wf_env_ext_map := X.(wf_env_map) |};
 abstract_primitive_constant X := abstract_primitive_constant X.(wf_env_ext_reference);
 abstract_env_rel X := abstract_env_rel X.(wf_env_reference) ;
 abstract_pop_decls := optim_pop ;
 |}.
Next Obligation.
  pose proof (X.(wf_env_reference).(reference_impl_wf)) as [?].
  sq. destruct (H _ eq_refl).
  apply EnvMap.repr_add; eauto; try eapply wf_fresh_globals; eauto.
  destruct X1; eauto.
  apply wf_env_map_repr.
Qed.
Next Obligation. apply wf_env_map_repr. Qed.

Section WfEnv.
  Context {cf : checker_flags} {guard : abstract_guard_impl}.

  Definition reference_impl_sq_wf (Σ : reference_impl_ext) : ∥ wf Σ ∥.
  Proof using Type.
    destruct (reference_impl_ext_wf Σ).
    sq. apply X.
  Qed.

  Definition lookup (Σ : wf_env_ext) (kn : kername) : option global_decl :=
    EnvMap.lookup kn Σ.(wf_env_ext_map).

  Lemma lookup_lookup_env Σ kn : lookup Σ kn = lookup_env Σ kn.
  Proof using Type.
    rewrite /lookup. destruct Σ as [Σ map repr]. pose (reference_impl_sq_wf Σ).
    sq. apply EnvMap.lookup_spec; auto. now eapply wf_fresh_globals.
  Qed.

End WfEnv.

Create HintDb wf_env discriminated.
Global Hint Constants Opaque : wf_env.
Global Hint Variables Opaque : wf_env.

Global Hint Resolve reference_impl_ext_wf : wf_env.
Global Hint Resolve reference_impl_wf : wf_env.

Definition Σudecl_ref {cf : checker_flags} {guard : abstract_guard_impl} (Σ : reference_impl_ext) :
  ∥ on_udecl Σ.(reference_impl_env_ext).1 Σ.(reference_impl_env_ext).2 ∥ :=
    map_squash (fun x => x.2) Σ.

Definition Σudecl {cf : checker_flags} {guard : abstract_guard_impl} (Σ : wf_env_ext) :
  ∥ on_udecl Σ.(reference_impl_env_ext).1 Σ.(reference_impl_env_ext).2 ∥ :=
  map_squash (fun x => x.2) Σ.

  Global Hint Resolve Σudecl : wf_env.

Ltac wf_env := auto with wf_env.

(** Build an optimized environment representation for lookups along with the graph associated to a well-formed
  global environment. The graph building is separated, so that [(build_wf_env_ext Σ wfΣ).(wf_env_ext_env)] is
  convertible to [Σ]. *)

Definition build_wf_env_ext {cf : checker_flags} {guard : abstract_guard_impl} (Σ : global_env_ext) (wfΣ : ∥ wf_ext Σ ∥) : wf_env_ext :=
  {| wf_env_ext_reference :=
      {| reference_impl_env_ext := Σ; reference_impl_ext_wf := wfΣ |} ;
     wf_env_ext_map := EnvMap.of_global_env Σ.(declarations);
     wf_env_ext_map_repr := EnvMap.repr_global_env Σ.(declarations);
|}.

Section GraphSpec.
  Context {cf:checker_flags} {guard : abstract_guard_impl} {Σ : global_env_ext} (HΣ : ∥ wf Σ ∥)
      (Hφ : ∥ on_udecl Σ.1 Σ.2 ∥)
      (G : universes_graph) (HG : is_graph_of_uctx G (global_ext_uctx Σ)).

  Local Definition HΣ' : ∥ wf_ext Σ ∥.
  Proof.
    destruct HΣ, Hφ; now constructor.
  Qed.

  Lemma is_graph_of_uctx_levels (l : Level.t) :
    LevelSet.mem l (uGraph.wGraph.V G) <->
    LevelSet.mem l (global_ext_levels Σ).
  Proof using HG.
    unfold is_graph_of_uctx in HG.
    case_eq (gc_of_uctx (global_ext_uctx Σ)); [intros [lvs cts] XX|intro XX];
      rewrite -> XX in *; simpl in *; [|contradiction].
    unfold gc_of_uctx in XX; simpl in XX.
    destruct (gc_of_constraints Σ); [|discriminate].
    inversion XX; subst.
    unfold is_true. rewrite !LevelSet.mem_spec.
    symmetry. apply HG.
  Qed.

End GraphSpec.

Program Global Instance canonical_abstract_env_prop {cf:checker_flags} {guard : abstract_guard_impl} :
  @abstract_env_prop _ _ _ canonical_abstract_env_struct :=
     {| abstract_env_ext_exists := fun Σ => sq (reference_impl_env_ext Σ ; eq_refl); |}.
Next Obligation. wf_env. Qed.
Next Obligation. now sq. Qed.
Next Obligation. wf_env. Qed.
Next Obligation. now split. Qed.
Next Obligation.
  apply (reference_pop_decls_correct X decls prf X (reference_pop X) eq_refl eq_refl).
Qed.
Next Obligation.
  epose proof (HΣ := reference_impl_ext_wf X). sq.
  apply lookup_global_Some_iff_In_NoDup => //.
  destruct HΣ as [[] _]. now eapply NoDup_on_global_decls.
Qed.
Next Obligation.
  pose proof (reference_impl_ext_wf X); sq.
  set (uctx := wf_ext_gc_of_uctx _) in *; destruct uctx as [[lc ctrs] Huctx].
  assert (consistent (global_ext_uctx X).2) as HC.
      { sq; apply (global_ext_uctx_consistent _ H). }
  simpl in HC. apply gc_consistent_iff in HC.
  eapply leqb_level_n_spec; eauto.
    + eapply gc_of_uctx_invariants; try eapply wf_ext_global_uctx_invariants; eauto.
    + clear Hl Hl'. Opaque gc_of_constraints. cbn in *. Transparent gc_of_constraints.
      destruct (gc_of_constraints X); inversion Huctx. now destruct H2.
    + unfold reference_impl_ext_graph; cbn.
      set (G := graph_of_wf_ext _); destruct G as [G HG].
      cbn. unfold is_graph_of_uctx in HG. now rewrite Huctx in HG.
Qed.
Next Obligation. pose (reference_impl_ext_wf X). sq. symmetry; apply LevelSet.Raw.mem_spec. typeclasses eauto. Defined.
Next Obligation.
  pose (reference_impl_wf X). sq.
  rename H0 into Hudecl. rename H1 into Hudecl'.
  assert (H0 : global_uctx_invariants (global_uctx X)).
  { eapply wf_global_uctx_invariants; eauto. }
  set (udecl := (t , t0)).
  assert (H1 : global_uctx_invariants (ContextSet.union udecl (global_uctx X))).
  { split => //.
    - apply LevelSet.union_spec; right ; now destruct H0.
    - intros [[l ct] l'] [Hl|Hl]%CS.union_spec.
      + now specialize (Hudecl _ Hl).
      + destruct H0 as [_ H0]. specialize (H0 _ Hl).
        split; apply LevelSet.union_spec; right;
        now cbn in H0.
     }
  unfold reference_impl_graph; rewrite andb_and.
  pose proof (reference_impl_graph_wf X) as HG.
  set (gph := (graph_of_wf X).π1) in *. clearbody gph. simpl in HG.
  pose proof (HG' := is_graph_of_uctx_add Hudecl' HG).
  pose (global_ext_uctx := ContextSet.union udecl (global_uctx X)).
  pose (wf_consistent_extension_on_consistent udecl.2 s).
  assert (reorder : forall a a' b c : Prop, (b -> a) -> (a /\ b <-> a' /\ c) -> b <-> a' /\ c) by intuition; eapply reorder; try eassumption; clear reorder.
  rewrite - (is_consistent_spec global_ext_uctx) (is_consistent_spec2 HG').
  assert (reorder : forall a b c : Prop, (a -> b <-> c) -> a /\ b <-> a /\ c) by intuition; apply reorder.
  move=> ?; rewrite consistent_extension_on_union.
  1:{ pose proof (reference_impl_wf X); sq.
      apply: PCUICUnivSubstitutionConv.levels_global_constraint. }
  cbn.
  change (CS.union _ _) with global_ext_uctx.2.
  apply: consistent_ext_on_full_ext=> //.
  apply: add_uctx_subgraph.
Qed.
Next Obligation. apply guard_correct. Qed.

Program Global Instance optimized_abstract_env_prop {cf:checker_flags} {guard : abstract_guard_impl} :
  @abstract_env_prop _ _ _ optimized_abstract_env_struct :=
     {| abstract_env_ext_exists := fun Σ => sq (reference_impl_env_ext Σ ; eq_refl); |}.
Next Obligation. wf_env. Qed.
Next Obligation. now sq. Qed.
Next Obligation. wf_env. Qed.
Next Obligation. now split. Qed.
Next Obligation. unfold optim_pop. set (optim_pop_obligation_1 cf X). clearbody r.
  pose proof (reference_pop_decls_correct X decls prf X (reference_pop X) eq_refl eq_refl).
  specialize (prf _ eq_refl).
  destruct (declarations X); cbn; inversion prf; inversion H0. subst.
  now destruct x.
Qed.
Next Obligation.
  epose proof (HΣ := reference_impl_ext_wf X). sq.
  etransitivity; try apply abstract_env_lookup_correct => //.
  assert (lookup_env X kn = EnvMap.lookup kn X).
  { erewrite EnvMap.lookup_spec; try reflexivity.
    1: apply wf_fresh_globals; eauto.
    1: apply wf_env_ext_map_repr. }
  now rewrite <- H.
Qed.
Next Obligation.
    revert n l l' Hl Hl'. erewrite wf_ext_gc_of_uctx_irr.
    exact (abstract_env_leqb_level_n_correct X.(wf_env_ext_reference) eq_refl).
Qed.
Next Obligation.
  now erewrite (abstract_env_level_mem_correct X.(wf_env_ext_reference)).
Qed.
Next Obligation.
  now erewrite (abstract_env_is_consistent_correct X.(wf_env_reference)) with (udecl := (t,t0)); eauto.
Qed.
Next Obligation. eapply guard_correct. Qed.

Definition canonical_abstract_env_impl {cf:checker_flags} {guard : abstract_guard_impl} : abstract_env_impl :=
  (reference_impl ; reference_impl_ext ; canonical_abstract_env_struct ; canonical_abstract_env_prop).

Definition optimized_abstract_env_impl {cf:checker_flags} {guard : abstract_guard_impl} : abstract_env_impl :=
  (wf_env; wf_env_ext ; optimized_abstract_env_struct ; optimized_abstract_env_prop).

Definition build_wf_env_from_env {cf : checker_flags} (Σ : global_env) (wfΣ : ∥ PCUICTyping.wf Σ ∥) : wf_env
  :=
  let Σm := EnvMap.of_global_env Σ.(declarations) in
  {| wf_env_reference := {| reference_impl_env := Σ; reference_impl_wf := wfΣ |} ;
     wf_env_map := Σm;
     wf_env_map_repr := EnvMap.repr_global_env Σ.(declarations);
 |}.

author: MetaCoq

repo: metacoq

save_path: github-repos/coq/MetaCoq-metacoq