The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

I agree that the atoms should be opaque, hence how I knew there was a
problem when I hit an attempt to match against an atom within the
reflection procedure (after uselessly making a bunch of functions along
the way to that point transparent).

I've attached the now working reflection code as a stand-alone .v file,
so that you can judge if it does reflection properly.  There are
example tests at the end.  I used Coq 8.12beta1, but it should work on
earlier versions, as there is nothing new-Coq-ish about it.

If some are interested in where it went wrong as I described, I can
create a version that demonstrates the problem.  However, I think the
problem can be re-created as follows - by performing "simpl in *.
rewrite flatten_correct." a few steps earlier within the backward
function.  If the second "-" subgoal solution in backward is changed
from:

    - destruct (backward_flat (flatten lf) k) as [H|]. 2:right.
      left. intros. simpl in *. rewrite flatten_correct. apply H.
      assumption.

to:

    - destruct (backward_flat (flatten lf) k) as [H|]. 2:right.
      simpl in *. rewrite flatten_correct.
      left. intros. apply H. assumption.

and then flatten_correct and all of its dependencies are made
transparent, eventually one ends up with app_nil_r matching against
list atom.  Note that the "left" tactic, as the goal is an option type,
shifts here from being executable code to non-executable code.

In the attached working version, I reverted all of the functions I had
previously made transparent to being oapque - they obviously (now, at
least) don't need to be transparent based on what they are proving, and
thinking that they did need to be transparent is what led me down the
rabbit hole until I hit the match against an atom I described.

On Tue, 30 Jun 2020 09:59:59 +0200
Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

> Le 29/06/2020 à 21:21, jonikelee AT gmail.com a écrit :
> 
> > I just learned an interesting lesson about writing decision
> > procedures using reflection in Coq.  It's probably one that others
> > have encountered before - so "tl;dr" if this is a familiar refrain:
> > functions used within reflection procedures are not the only
> > elements where transparency (Defined vs. Qed) needs to be
> > considered.  Atoms matter, too.  
> 
> You seem to be using a rather peculiar definition of reflection. Atoms
> should be opaque, by definition. Or rather, since the ability to
> distinguish atoms is critical for most decision procedures, atoms
> should just be addresses (e.g., closed integers generated by a gensym
> function). For example, a decision procedure on propositional logic
> will manipulate terms of the following type:
> 
> Inductive term : Set :=
>   | Atom (n : nat)
>   | Neg (t : term)
>   | And (t1 t2 : term).
> 
> An object of type term is necessarily closed, unless your reification
> procedure contains a bug. As a consequence, your computations should
> never get stuck.
> 
> From reading your email, I am under the impression that your Atom
> constructor takes an argument that comes directly from the original
> goal or hypotheses. If so, this no longer qualifies as reflection.
> 
> Best regards,
> 
> Guillaume

(**** [uses Coq 8.12beta1]
Reflection procedure for sorted (=LocallySorted lt) solves goals of the form:
  forall (a b : A)(p q r : list A), 
  sorted(a::p++q++r) -> sorted(p++r++[b]) -> sorted(q++[b]) -> a<b ->
  sorted(p++q++r++[b]).
where A is an ordered class.
****)

Set Default Goal Selector "all".

Require Export Coq.Classes.RelationClasses.

Class Ordered(A : Set) :=
  { lt : A -> A -> Prop;
    lt_strict :> StrictOrder lt
  }.

Require Import Coq.Lists.List.
Import ListNotations.
Require Export Coq.Sorting.Sorted.

Notation sorted := (LocallySorted lt).

Infix "<" := lt (at level 70) : list_scope.

Definition nat_eq_dec(i j:nat) : {i=j}+{i<>j}.
Proof.
  decide equality.
Defined.

Definition natpair_eq_dec : forall (i j :nat*nat), {i=j}+{i<>j}.
Proof.
  decide equality.
  apply nat_eq_dec.
Defined.

(*use option for partial computation of reflection results*)
Notation "[ P ]" := (option P) : type_scope.

Definition optOut (X : Type) (x : [X]) : if x then X else True :=
  match x with
  | Some Y => Y
  | None => I
  end.

(*the only reified lists are args to the sorted predicate - the atoms within these lists
  are both list atoms [LF_list] and element atoms [LF_cons]*)
Inductive List_formula :=
| LF_nil : List_formula
| LF_cons : nat -> List_formula -> List_formula
| LF_list : nat -> List_formula
| LF_app : List_formula -> List_formula -> List_formula.

Inductive Sorted_formula :=
| SF_lt : nat -> nat -> Sorted_formula (*a<b*)
| SF_sorted : List_formula -> Sorted_formula
| SF_and : Sorted_formula -> Sorted_formula -> Sorted_formula
| SF_or : Sorted_formula -> Sorted_formula -> Sorted_formula
| SF_imp : Sorted_formula -> Sorted_formula -> Sorted_formula
| SF_flat : list nat -> Sorted_formula (*used internally only*)
| SF_skip : Prop -> Sorted_formula. (*unreified props*)

Section defs.
  Context {A : Set}.
  Context {ordA : Ordered A}.

  Inductive Atom : Set := Aatom(_:A) | Latom(_:list A).

  Variable atomics : list Atom.

  Definition nthatom i := nth i atomics (Latom nil).

  Definition aDenote i :=
    match (nthatom i) with
    | Aatom a => [a]
    | Latom l => l
    end.

  Fixpoint lfDenote(lf : List_formula) : list A :=
    match lf with
    | LF_nil => nil
    | LF_cons i lf' => aDenote i ++ lfDenote lf'
    | LF_list i => aDenote i
    | LF_app lf1 lf2 => lfDenote lf1 ++ lfDenote lf2
    end.

  (*for flattened List_formula*)
  Fixpoint fDenote(l : list nat) : list A :=
    match l with
    | nil => nil
    | i::r => aDenote i ++ fDenote r
    end.

  Definition orderedAtoms x y := sorted (aDenote x ++ aDenote y).
  
  Infix "<#" := orderedAtoms (at level 70) : list_scope.

  Fixpoint sfDenote(sf : Sorted_formula) : Prop :=
    match sf with
    | SF_lt i j =>
      match (nthatom i), (nthatom j) with
      | Aatom a, Aatom b => a<b
      | _, _ => i <# j (*should not occur, but needed for correctness*)
      end
    | SF_sorted lf => sorted (lfDenote lf)
    | SF_and sf1 sf2 => sfDenote sf1 /\ sfDenote sf2
    | SF_or sf1 sf2 => sfDenote sf1 \/ sfDenote sf2
    | SF_imp sf1 sf2 => sfDenote sf1 -> sfDenote sf2
    | SF_flat l => sorted (fDenote l)
    | SF_skip p => p
    end.

  Fixpoint flatten(lf : List_formula) : list nat :=
    match lf with
    | LF_nil => nil
    | LF_cons i lf' => i :: flatten lf'
    | LF_list i => [i]
    | LF_app lf1 lf2 => flatten lf1 ++ flatten lf2
    end.

  (*simple structure for Known for now - easy to prove with, but bad performance*)
  Definition Known := list (nat * nat).

  Definition add_known(i j:nat)(k:Known) := (i,j)::k.

  Fixpoint add_knowns(i:nat)(js:list nat)(k:Known) {struct js} :=
    match js with
    | nil => k
    | j::js' => add_knowns i js' (add_known i j k)
    end.

  Fixpoint allOrdered(k:Known) : Prop :=
    match k with
    | nil => True
    | (i, j)::k' => i <# j /\ allOrdered k'
    end.

  Lemma allOrdered_add :
    forall i j k, allOrdered k -> i <# j -> allOrdered (add_known i j k).
  Proof.
    induction k. intros. hnf. tauto.
  Qed.

  
  (*lemmas about sorted - all are opaque*)

  Local Ltac triv := subst; try solve [eassumption | constructor; eassumption].

  Lemma sortedl : forall {l1 l2 : list A}, sorted (l1++l2) -> sorted l1.
  Proof with triv.
    induction l1 as [|a l1 IHl1]... 
    intros l2 H. destruct l1... 
    inversion H... 
    constructor...
    eapply IHl1...
  Qed.

  Lemma sortedr : forall {l1 l2 : list A}, sorted (l1++l2) -> sorted l2.
  Proof with triv.
    induction l1 as [|a l1 IHl1].
    intros l2 H... destruct l1.
    inversion H...
    eapply IHl1...
  Qed.

  Lemma sortedtail : forall {l : list A}{a : A}, sorted (a::l) -> sorted l.
  Proof with triv.
    intros l a H. inversion H...
  Qed.

  Lemma sortcomb : forall {l1 l2 : list A}{a : A},
                     sorted(l1++[a]) -> sorted(a::l2) -> sorted(l1++a::l2).
  Proof with triv.
    induction l1 as [|a l1 IHl1]. intros l2 ? H1 H2...
    destruct l1. simpl in *. constructor... inversion H1... apply IHl1...
  Qed.

  Lemma sortins : forall {l1 l2 l3 : list A}{a b : A},
                    sorted(l1++a::l2) ->
                    sorted(l2++b::l3) -> a<b ->
                    sorted(l1++a::l2++b::l3).
  Proof with triv.
    induction l1 as [|a l1 IHl1]. intros l2 l3 ? ? H H0 H1.
    - destruct l2... inversion H... 
    - destruct l1. simpl in *.
      inversion H. subst. constructor... eapply IHl1...
  Qed.

  Lemma desort : forall {l1 l2 : list A}{a b : A},
                     sorted (a::l1++b::l2) -> a<b.
  Proof with triv.
    induction l1 as [|a l1 IHl1]. intros ? ? ? H. inversion H... 
    transitivity a... eapply IHl1...
  Qed.

  Lemma sortedm : forall {l1 l2 l3 : list A},
                    sorted (l1++l2++l3) -> sorted (l1++l3).
  Proof with triv.
    induction l1 as [|a l1 IHl1]. intros l2 l3 H.
    - eapply sortedr...
    - destruct l1.
      + destruct l3... constructor.
        * do 2 apply sortedr in H...
        * apply desort in H...
      + inversion H... simpl. constructor... eapply IHl1...
  Qed.

  Lemma sorted3way :
    forall l1 l2 l3, sorted(l1++l2) -> sorted(l2++l3) -> sorted(l1++l3) -> sorted(l1++l2++l3).
  Proof.
    intros l1 [] [] H1 H2 H3. simpl in *. rewrite ?app_nil_r in *. try assumption.
    pose proof (desort H2) as H. apply sortedtail in H2. apply (sortins H1 H2 H).
  Qed.

  
  (*flatten list args to the sorted predicate internally for convenience*)

  Lemma flatten_app : forall l1 l2, fDenote (l1++l2) = fDenote l1 ++ fDenote l2.
  Proof.
    induction l1. intro l2. simpl.
    - reflexivity.
    - rewrite <-app_assoc. f_equal. apply IHl1.
  Qed.

  Lemma flatten_correct: forall lf, lfDenote lf = fDenote (flatten lf).
  Proof.
    induction lf. simpl. rewrite ?flatten_app. 3:apply app_nil_end. congruence.
  Qed.

  (*more opaque lemmas about sorted, but now mixing in flattened list formulas*)
  
  Lemma sorted_push:
    forall x l, (forall y, In y l -> x <# y) ->
                sorted (aDenote x) -> sorted (fDenote l) -> sorted (fDenote (x::l)).
  Proof.
    induction l as [ |i l IHl]. intros H H1 H2. simpl.
    - rewrite app_nil_r. assumption.
    - apply sorted3way.
      + apply H. simpl. tauto.
      + exact H2.
      + apply IHl.
        * intros y H3. apply H. simpl. tauto.
        * assumption.
        * simpl in H2. apply sortedr in H2. exact H2.
  Qed.

  Lemma sorted12: forall i j, i <# j -> sorted (aDenote i) /\ sorted (aDenote j).
  Proof.
    intros i j IJ. unfold orderedAtoms in IJ.
    pose proof (sortedl IJ). pose proof (sortedr IJ). tauto.
  Qed.

  Lemma sortedfhead : forall i j js, sorted (fDenote (i :: j :: js)) -> i <# j.
  Proof.
    simpl. intros i j js. rewrite app_assoc. apply sortedl.
  Qed.

  Lemma sortedfmid: forall i j js, sorted (fDenote (i :: j :: js)) -> sorted (fDenote (i::js)).
  Proof.
    simpl. intros i j js. apply sortedm.
  Qed.

  Lemma sortedin : forall l i j, sorted (fDenote (i :: l)) -> In j l -> i <# j.
  Proof.
    induction l as [|x l IHl]. intros i j H1 [].
    - apply sortedfhead in H1. congruence.
    - apply sortedfmid in H1. apply IHl. assumption.
  Qed.

  Lemma allOrdered_adds:
    forall i js k, allOrdered k -> sorted (fDenote (i::js)) -> allOrdered (add_knowns i js k).
  Proof.
    induction js. intros. simpl.
    - assumption.
    - apply IHjs.
      + simpl. intuition idtac. eapply sortedfhead. eassumption.
      + eapply sortedfmid. eassumption.
  Qed.

  
  (*The reflection procedure:*)

  (*k is Known, f is Sorted_formula*)
  Notation "k '-~>' f" := (allOrdered k -> sfDenote f) (at level 60) : type_scope.

  Fixpoint forward_flat f l (cont: forall k', [k' -~> f]) k {struct l} :
    [k -~> SF_imp (SF_flat l) f].
  Proof.
    destruct l as [ |i js]. simpl in *.
    - destruct (cont k) as [H| ]. 2:right.
      left. intros. apply H. assumption.
    - destruct (forward_flat f js cont (add_knowns i js k)) as [H| ]. 2:right.
      left. intros H1 H2. simpl in H. apply H.
      * apply allOrdered_adds. assumption.
      * apply sortedr in H2. exact H2.
  Defined.
  
  Fixpoint forward f hyp (cont: forall k', [k' -~> f]) k : [k -~> SF_imp hyp f].
  Proof with [>left;simpl in *; tauto|right].
    destruct hyp as [i j|lf|h1 h2|h1 h2|h1 h2|l|p].
    - destruct (cont (add_known i j k)) as [H| ]. 2:right.
      left. simpl in *. intros. apply H. intuition idtac.
      unfold orderedAtoms in *. unfold aDenote in *.
      destruct (nthatom i), (nthatom j). repeat constructor. assumption.
    - destruct (forward_flat f (flatten lf) cont k) as [H| ]. 2:right.
      left. simpl in *. intros H1 H2. apply (H H1). rewrite <-flatten_correct. assumption.
    - destruct (forward (SF_imp h2 f) h1 (forward f h2 cont) k) as [H| ]...
    - destruct (forward f h1 cont k) as [H| ]. 2:right.
      destruct (forward f h2 cont k) as [H'| ]...
    - destruct (cont k) as [H| ]...
    - apply (forward_flat f l cont k).
    - destruct (cont k) as [H| ]...
  Defined.

  Fixpoint In_part x (k : Known) : [In x k].
    destruct k as [ |y k']. 1:right.
    destruct (natpair_eq_dec x y).
      + subst. simpl. left. left. reflexivity.
      + destruct (In_part x k'). 2:right.
        simpl. left. right. assumption.
  Defined.

  Fixpoint All_in_part i (l : list nat)(k : Known) : [forall j, In j l -> In (i,j) k].
  Proof.
    destruct l as [|x l]. 
    - left. intros j [].
    - destruct (All_in_part i l k) as [IHl|]. 2:right.
      destruct (In_part (i,x) k) as [H|]. 2:right.
      left. intros j H1.
      destruct H1 as [H1|H1].
      + subst. assumption.
      + apply IHl. assumption.
  Defined.

  Lemma in_allOrdered : forall k i j, In (i, j) k -> allOrdered k -> i <# j.
  Proof.
    induction k as [|a k]. intros i j.
    - simpl. contradiction.
    - simpl. intros [->|].
      + tauto.
      + intros. apply IHk.
        * assumption.
        * destruct a. tauto.
  Qed.

  Fixpoint All_ordered i (l : list nat)(k : Known) :
    [allOrdered k -> sorted (fDenote l) -> forall j, In j l -> i <# j].
  Proof.
    destruct l as [|x l].
    - left. intros H j S [].
    - destruct (In_part (i,x) k) as [H|]. 2:shelve.
      case_eq (nthatom x). intros X E.
      { left. intros H0 S j [->|H1].
        - apply (in_allOrdered k i j). assumption.
        - apply in_allOrdered in H. 2:assumption.
          eapply sortedin. 2:eassumption.
          simpl in S. hnf in H.
          replace (aDenote x) with ([X]) in H, S by
              (unfold aDenote;rewrite E;reflexivity).
          apply (@sortedm _ [X] _ (sortcomb H S)). }
      destruct (All_ordered i l k) as [IHl|]. 2:right.
      + left. intros H0 S j [->|H1].
        * apply (in_allOrdered k i j). assumption.
        * simpl in S. apply sortedr in S. apply IHl. assumption.
    Unshelve.
    (*TBD: do transitive closure cases here*)
    right.
  Defined.

  Fixpoint In1_part i (k: Known) : option {j | In (i,j) k \/ In (j,i) k}.
  Proof. 
    destruct k as [|x k]. 1:right.
    destruct x as (x,y). destruct (nat_eq_dec x i).
    { subst. left. exists y. simpl. tauto. }
    destruct (nat_eq_dec y i).
    { subst. left. exists x. simpl. tauto. }
    destruct (In1_part i k)  as [[j H]|]. 2:right.
    left. exists j. simpl. tauto.
  Defined.

  Fixpoint backward_flat l k : [k -~> SF_flat l].
  Proof.
    destruct l as [|i l]. simpl.
    - left. intros. constructor.
    - destruct (backward_flat l k) as[H|]. 2:right.
      destruct (All_ordered i l k) as [H1|]. 2:right.
      case_eq (nthatom i). intros a N.
      + assert (sorted (aDenote i)) as Q.
        { unfold aDenote. rewrite N. constructor. }
        left. intro H0. apply (sorted_push i l (H1 H0 (H H0))). tauto.
      + assert (option (allOrdered k -> sorted (aDenote i))) as Q.
        { destruct (In1_part i k) as [[j X]|]. 2:right.
          left. intro H2. destruct X as [X|X].
          apply (sorted12 _ _ (in_allOrdered _ _ _ X H2)). }
        destruct Q as [Q|]. 2:right.
        left. intro H0. apply (sorted_push i l (H1 H0 (H H0))). tauto.
  Defined.
  
  Fixpoint backward f k : [k -~> f].
  Proof.
    destruct f as [i j|lf|f1 f2|f1 f2|f1 f2|l|p].
    - destruct (In_part (i,j) k) as [H|]. 2:right.
      left. intro H0. pose proof (in_allOrdered _ _ _ H H0) as H1.
      simpl. unfold orderedAtoms in *. unfold aDenote in *.
      destruct (nthatom i), (nthatom j). try assumption.
      inversion H1. assumption.
    - destruct (backward_flat (flatten lf) k) as [H|]. 2:right.
      left. intros. simpl in *. rewrite flatten_correct. apply H. assumption.
    - destruct (backward f1 k) as [H|]. 2:right.
      destruct (backward f2 k) as [H'|]. 2:right.
      left. simpl. tauto.
    - destruct (backward f1 k) as [H|].
      + left. simpl. tauto.
      + destruct (backward f2 k) as [H|]. 2:right.
        left. simpl. tauto.
    - apply (forward f2 f1 (backward f2) k).
    - apply backward_flat.
    - right.
  Defined.

  Definition solve_sorted : forall f, [sfDenote f].
    intro f. destruct (backward f nil). 2:right. simpl in *. left. tauto.
  Defined.

  Definition reflect_sorted f := optOut _ (solve_sorted f).
End defs.


(*Reification tactics*)

Ltac inList x xs :=
  match xs with
    | nil => false
    | Aatom x::_ => true
    | Latom x::_ => true
    | _::?xs' => inList x xs'
  end.

Ltac lookup x xs :=
  lazymatch xs with
  | Aatom x::_ => constr:(0)
  | Latom x::_ => constr:(0)
  | _::?xs' =>
    let n := lookup x xs' in
    constr:(S n)
  | _ => fail 999 "lookup failed for" x
  end.

Ltac nlookup n xs :=
  match xs with
  | ?x::?xs' =>
    match n with
    | 0 => x
    | S ?n' => nlookup n' xs'
    end
  end.

Ltac addToList A x xs :=
  let b := inList x xs in
    match b with
      | true => xs
      | false =>
        match type of x with
        | A => constr:((@Aatom A x)::xs)
        | list A => constr:((@Latom A x)::xs)
        | _ => xs
        end
    end.

Ltac allVarsList A xs l :=
  match l with
  | nil => xs
  | ?a :: ?l =>
    let xs := allVarsList A xs a in
    allVarsList A xs l
  | ?l1 ++ ?l2 =>
    let xs := allVarsList A xs l1 in
    allVarsList A xs l2
  | ?v => let d:=constr:(ltac:(is_var v;exact I)) in addToList A v xs
  | _ =>
    let d:=constr:(ltac:(idtac "allVarsList failed to match" l;exact I)) in
    addToList A l xs
  end.

Ltac allVars A xs e :=
  lazymatch e with
    | ?e1 /\ ?e2 =>
      let xs := allVars A xs e1 in
        allVars A xs e2
    | ?e1 \/ ?e2 =>
      let xs := allVars A xs e1 in
        allVars A xs e2
    | ?e1 -> ?e2 =>
      let xs := allVars A xs e1 in
      allVars A xs e2
    | ?a < ?b =>
      let xs := addToList A a xs in
      addToList A b xs
    | sorted ?l => allVarsList A xs l
    | _ => addToList A e xs
  end.

Ltac reifyList xs l :=
  match l with
  | nil => constr:(LF_nil)
  | ?l1 ++ ?l2 =>
    let lf1 := reifyList xs l1 in
    let lf2 := reifyList xs l2 in
    constr:(LF_app lf1 lf2)
  | ?a :: ?t =>
    let i := lookup a xs in
    let lf := reifyList xs t in
    constr:(LF_cons i lf)
  | ?v =>
    let i := lookup v xs in
    constr:(LF_list i)
  | _ => fail 999 "reifyList failed with" l
  end.

Ltac reifyTerm xs e :=
  lazymatch e with
    | ?e1 /\ ?e2 =>
      let p1 := reifyTerm xs e1 in
      let p2 := reifyTerm xs e2 in
        constr:(SF_and p1 p2)
    | ?e1 \/ ?e2 =>
      let p1 := reifyTerm xs e1 in
      let p2 := reifyTerm xs e2 in
        constr:(SF_or p1 p2)
    | ?e1 -> ?e2 =>
      let p1 := reifyTerm xs e1 in
      let p2 := reifyTerm xs e2 in
      constr:(SF_imp p1 p2)
    | ?a < ?b =>
      let na := lookup a xs in
      let nb := lookup b xs in
      constr:(SF_lt na nb)
    | sorted ?l =>
      let lf := reifyList xs l in
      constr:(SF_sorted lf)
    | _ =>
      constr:(SF_skip e)
  end.

(*Solver tactic, X is the element type:*)

Ltac solve_sorted_on X :=
  intros;
  repeat (*revert reifiable hyps only*)
    match goal with
    | H : sorted ?L |- _ =>
      lazymatch type of L with
      | list X => revert H
      end
    | H : ?a < ?b |- _ =>
      lazymatch type of a with
      | X => revert H
      end
    | H : _ /\ _ |- _ => revert H
    | H : _ \/ _ |- _ => revert H
    end;
  lazymatch goal with
    |- ?G =>
    let atoms := allVars X constr:(nil:list (@Atom X)) G in
    let atoms := eval simpl in atoms in (*not needed, but makes it easier to read*)
    let f := reifyTerm atoms G in
    exact (@reflect_sorted X _ atoms f)
  end.

Ltac solve_sorted :=
  (*hack to determine the element type X - only works for some goals:*)
  intros;
  lazymatch goal with
  | |- sorted ?L =>
    lazymatch type of L with
    | list ?X => solve_sorted_on X
    end
  | |- ?a < ?b =>
    let X := type of a in solve_sorted_on X
  end.


Section Examples.

  Context {A : Set}.
  Context {ordA : Ordered A}.

  Lemma realeasy: forall a l, sorted (a::l) -> sorted (a::l).
  Proof.
    time solve_sorted.
  Qed.
  Print realeasy.
  
  Lemma nolistatoms: forall a b c d e f,
      sorted (a::(b::(c::d::nil)++e::nil)++f::nil) -> sorted(a::c::f::nil).
  Proof.
    time solve_sorted.
  Qed.
  Print nolistatoms.
  (*note that opaque dependencies includes dependencies that don't block reduction,
    hence it isn't very useful for finding opaque functions that do block reduction*)
  Print Opaque Dependencies nolistatoms.
  
  Lemma listsonly: forall p q r, sorted(p++q++r) -> sorted(p++r).
  Proof.
    time solve_sorted.
  Qed.
  Print listsonly.

  Lemma ltonly: forall a b, a<b -> a<b.
  Proof.
    solve_sorted.
  Qed.
  Print ltonly.

  (*The algorithm in All_ordered does not yet include transitive closure:*)
  Lemma notransitivityyet: forall a b c, a<b -> b<c -> a<c.
  Proof.
    Fail solve_sorted.
  Abort.
  
  Lemma interesting:
    forall a b p q r, sorted(a::p++q++r) -> sorted(p++r++[b]) -> sorted(q++[b]) -> a<b ->
                      sorted(p++q++r++[b]).
  Proof.
    time solve_sorted.
  Qed.
  Print interesting.

  (*the slowness here is mostly due to the simplistic structure of Known*)
  Lemma slooooow:
    forall p q r s t u v a b c d e f l,
      sorted(p++[a]++(q++[b])++r++l++([c]++(s++[d])++t++[e])++(u++[f])++v) ->
      sorted(q++([c]++t)++[e]++v).
  Proof.
    time solve_sorted.
  Qed.
  Print slooooow.

End Examples.