Sorted.v

Sorted.v

Require Import List.

Definition relation (X : Type) := X -> X -> Prop.
Check le : nat -> nat -> Prop.
Check le : relation nat.

Inductive HdRel {X : Type} (R : relation X) : X -> list X -> Prop :=
  | HdRel_nil  : forall x, HdRel R x nil
  | HdRel_cons : forall x y xs, R x y -> HdRel R x (y :: xs).

Inductive Sorted {X : Type} (R : relation X) : list X -> Prop :=
  | Sorted_nil  : Sorted R nil
  | Sorted_cons : forall x xs, Sorted R xs -> HdRel R x xs -> Sorted R (x :: xs).

Example sorted_nil:
  Sorted le (@nil nat).
Proof.               (* 1 subgoal: Sorted le nil *)
  apply Sorted_nil.  (* 0 subgoals *)
Qed.

Example sorted_list:
  Sorted le (1::2::nil).
Proof.                (* 1 subgoal: Sorted le (1 :: 2 :: nil) *)
  apply Sorted_cons.  (* 2 subgoals: Sorted le (2 :: nil)
                                     HdRel le 1 (2 :: nil) *)
  apply Sorted_cons.  (* 3 subgoals: Sorted le nil
                                     HdRel le 2 nil
                                     HdRel le 1 (2 :: nil) *)
  apply Sorted_nil.   (* 2 subgoals: HdRel le 2 nil
                                     HdRel le 1 (2 :: nil) *)
  apply HdRel_nil.    (* 1 subgoal: HdRel le 1 (2 :: nil) *)
  apply HdRel_cons.   (* 1 subgoal: 1 <= 2 *)
  Print le.           (* Inductive le (n : nat) : nat -> Prop :=
                         | le_n : n <= n 
                         | le_S : forall m : nat, n <= m -> n <= S m *)
  apply le_S.         (* 1 subgoal: 1 <= 1 *)
  apply le_n.         (* 0 subgoals *)
Qed.

Example unsorted_list:
  Sorted le (2::1::nil).
Proof.                (* 1 subgoal: Sorted le (2 :: 1 :: nil) *)
  apply Sorted_cons.  (* 2 subgoals: Sorted le (1 :: nil)
                                     HdRel le 2 (1 :: nil) *)
  apply Sorted_cons.  (* 3 subgoals: Sorted le nil
                                     HdRel le 1 nil
                                     HdRel le 2 (1 :: nil) *)
  apply Sorted_nil.   (* 2 subgoals: HdRel le 1 nil
                                     HdRel le 2 (1 :: nil) *)
  apply HdRel_nil.    (* 1 subgoals: HdRel le 2 (1 :: nil) *)
  apply HdRel_cons.   (* 1 subgoal: 2 <= 1 *)
  apply le_S.         (* 1 subgoal: 2 <= 0 *)
  (* apply le_S.      (* Error: Impossible to unify "?1219 <= S ?1220" with "2 <= 0". *) *)
Abort.