ordsample.v

Require Import List.
Import ListNotations.

Set Implicit Arguments.

(* begin hide *)

Definition is_true x := x = true.

Coercion is_true : bool >-> Sortclass.

Lemma sumbool_if_true : forall T T' (P : Prop)(H : sumbool P (~ P)) (f : T -> T') x y,
  P -> f (if H then x else y) = f x.
Proof with simpl in *.
  intros.
  destruct H; tauto.
Qed.

Lemma sumbool_if_false : forall T T' (P : Prop)(H : sumbool P (~ P)) (f : T -> T') x y,
  (~ P) -> f (if H then x else y) = f y.
Proof.
  intros.
  destruct H; tauto.
Qed.

Lemma sumbool_if_const : forall T (P : Prop)(H : sumbool P (~ P)) (x : T),
  (if H then x else x) = x.
Proof.
  intros. destruct H; auto.
Qed.

Lemma sumbool_impl : forall P Q : Prop, (P <-> Q) -> sumbool P (~ P) -> sumbool Q (~ Q).
Proof.
  intros. destruct H.
  destruct H0. left. auto.
  right. intro. apply n. auto.
Defined.

Lemma sumbool_if_impl : forall T (P Q : Prop)(H : sumbool P (~ P))(H0 : P <-> Q) (x y : T),
  (if H then x else y) = (if sumbool_impl H0 H then x else y).
Proof.
  intros.
  destruct H; destruct H0; simpl in *; auto.
Qed.

Ltac if_dest := repeat (
  match goal with
  | H : context[if ?X then _ else _] |- _ => destruct X
  | |- context[if ?X then _ else _] => destruct X
  end).
  
(* end hide *)

Section Defs.
(** * Basic definitions
We recall the definition of (strict) partial orders. Let [A] be a set and consider a binary relation [R] on [A].
*)
Variable A : Set.
Variable R : A -> A -> bool.

(**
We say [R] is anti reflexive, asymmetric, and transitive if [R] satisfies the followings, respectivery:
*)
Definition anti_refl := forall x, ~ R x x.
Definition asymm := forall x y, R x y -> ~ R y x.
Definition transitive := forall x y z, R x y -> R y z -> R x z.

(**
[R] is (strict) partial order if it is anti reflexive, anti symmetric, and transitive.
*)
Definition is_order := anti_refl /\ asymm /\ transitive.

End Defs.

Section Orders.

(** * Orders for term rewriting
Suppose [A] is a set on which equality is decidable.
*)
Variable A : Set.
Variable Aeq_dec : forall x y : A, sumbool (x = y) (x <> y).

(**
For a list on [A] [l], we define a partial order [ord_of_list l] on [A] with a helper function [ord_of_list' l].
*)
Fixpoint ord_of_list' l x y :=
  match l with
  | [] => false
  | z::l' => if Aeq_dec x z then true
    else if Aeq_dec y z then false else ord_of_list' l' x y
  end.

Definition ord_of_list l x y :=
  if Aeq_dec x y then false else ord_of_list' l x y.

(**
Let us show [ord_of_list l] is a partial order for any list [l]. First, we prove the anti reflexivity of [ord_of_list l].
*)
Lemma ord_of_list_anti_refl : forall l, anti_refl (ord_of_list l).
Proof.
  unfold anti_refl, ord_of_list. intros.
  (** Since [x = x], the if-then-else expression in [ord_of_list] returns false and it concludes the anti reflexivity. *)
  rewrite sumbool_if_true; congruence.
Qed.

(**
Next we check the asymmetricity, [ord_of_list l x y -> ~ (ord_of_list l y x)].
*)
Lemma ord_of_list_asymm : forall l, asymm (ord_of_list l).
Proof.
  unfold asymm, ord_of_list.
  (** We prove by induction on [l]. *)
  intros. induction l; intros; simpl in *.
  - (** In the case [l = []], [ord_of_list' []] rewrites to false. So in any case of [Aeq_dec y x], [ord_of_list []] returns false. *)
    rewrite sumbool_if_const. congruence.
  - (** Consider the case [l = a :: l]. *)
    destruct (Aeq_dec y x).
    + (** If [y = x], [ord_of_list (a :: l) y x] in the conclusion rewrites to false and so the asymmetricity holds. *) congruence.
    + (** Suppose [y <> x]. Then [ord_of_list (a :: l) x y] in hypothesis rewrites to
<<
 if Aeq_dec x a
     then true
     else if Aeq_dec y a then false else ord_of_list' l x y
>>.
*)
      simpl in *. rewrite sumbool_if_false in H; [|auto].
      (** We perform a case analysis on [Aeq_dec x a] and [Aeq_dec y a]. *)
      destruct (Aeq_dec x a); destruct (Aeq_dec y a).
      * (** In case [x = a] and [y = a], it contradicts due to the hypothesis [y <> x]. *)
        congruence.
      * (** In case [x = a] and [y <> a], [ord_of_list (a :: l) y x] in the conclusion rewrites to false. *)
        congruence.
      * (** In case [x <> a] and [y = a], [ord_of_list (a :: l) x y] in hypothesis rewrites to false. *)
        congruence.
      * (** In case [x <> a] and [y <> a], [ord_of_list (a :: l) x y] rewrites to [ord_of_list' l x y] and [ord_of_list (a :: l) y x)] rewrites to [ord_of_list' l y x]. The conclusion is proved using the induction hypothesis. *)
      apply IHl. rewrite sumbool_if_false; auto.
Qed.

(* We show the transitivity of [ord_of_list l], [ord_of_list l x y -> ord_of_list l y z -> ord_of_list x z]. *)
Lemma ord_of_list_trans : forall l, transitive (ord_of_list l).
Proof.
  unfold transitive, ord_of_list. intros.
  (** It is easily proved by similar case analysis and induction. *)
  induction l; simpl in *; if_dest; congruence || auto.
Qed.

(* Thus we have shown that [ord_of_list l] is a partial order. *)
Lemma ord_of_list_is_order : forall l, is_order (ord_of_list l).
Proof with simpl in *.
  intros. split; [|split].
  - apply ord_of_list_anti_refl.
  - apply ord_of_list_asymm.
  - apply ord_of_list_trans.
Qed.


Fixpoint lex (R : A -> A -> bool) (l1 l2 : list A) :=
  match l1, l2 with
  | x::xs, y::ys => if Aeq_dec x y then lex R xs ys else R x y
  | [], _::_ => true
  | _, _ => false
  end.

Lemma lex_is_ord : forall R, is_order R -> is_order (lex R).
Proof with simpl in *.
  unfold is_order, anti_refl, asymm, transitive.
  intros. destruct H as [H [H0 H1]].
  split; [|split].
  - induction x; simpl in *; [congruence|].
    if_dest; auto.
  - induction x; induction y; simpl in *; try congruence.
    if_dest; intros.
    + auto.
    + congruence.
    + congruence.
    + auto.
  - induction x; induction y; induction z; simpl in *; try congruence.
    intros. if_dest; try congruence; repeat subst.
    + eauto.
    + assert (R a0 a0) by eauto.
      apply H in H4. contradiction.
    + eauto.
Qed.

Lemma lex_fact : forall ord xs ys, lex ord xs ys ->
  (exists ys', ys = xs ++ ys') \/
  (exists zs, exists xs', exists ys', exists x, exists y,
    xs = zs ++ x :: xs' /\ ys = zs ++ y :: ys' /\ ord x y).
Proof with simpl in *.
  induction xs...
  - destruct ys; intros; simpl in *; [congruence|].
    left. exists (a :: ys). auto.
  - destruct ys; intros; simpl in *; [congruence|].
    if_dest.
    + subst. destruct (IHxs ys H).
      * left. destruct H0. exists x. congruence.
      * destruct H0 as [zs [xs' [ys' [x [y [H0 [H1 H2]]]]]]].
        repeat subst. right.
        exists (a0 :: zs). exists xs'. exists ys'. exists x. exists y. auto.
    + right. exists []... exists xs. exists ys. exists a. exists a0. auto.
Qed.

Lemma lex_fact2 : forall ord xs y ys, anti_refl ord -> lex ord xs (xs ++ y :: ys).
Proof with simpl in *.
  unfold anti_refl.
  induction xs; intros...
  - congruence.
  - if_dest; try congruence; auto.
Qed.

Definition my_ord l1 l2 := lex (ord_of_list l1) l1 l2.

Lemma my_ord_anti_refl_helper : forall xs l, ~ lex (ord_of_list l) xs xs.
Proof with simpl in *.
  induction xs; intros; simpl in *; [congruence|].
  if_dest...
  - auto.
  - set (H := ord_of_list_is_order).
    unfold is_order in H. destruct (H l). auto.
Qed.

End Orders.