The Coq mailing list

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

On Wed, 8 Jul 2020 17:21:06 -0400
Gregory Malecha <gregory AT bedrocksystems.com> wrote:

>...
> I don't think that this would be a very difficult translation to pull
> off. In most cases there is a mechanical translation.

I did it by hand - the result is attached.  And, as advertised, it
delivered considerable speedup. About 100x faster for that
"slooooow" test case.

But, I am curious about the mechanical translation from one proof style
to another.  Can you elaborate?

The decision procedure is still missing a transitive closure
component, though.  And that appears difficult to incorporate...

> 
> >  
> > >
> > > One thing that I've wanted for a while is the ability to control
> > > reduction with quoting and anti-quoting mechanisms a.la. meta
> > > programming. For example, something that would look roughly like
> > > this.
> > >
> > > Compute List.rev ((QUOTE (List.rev []) :: QUOTE (a ++ b) :: nil)
> > > ++ []). = [QUOTE (List.rev []); QUOTE (a ++ b)]
> > >
> > > Note that QUOTE semantically acts as id, but for the purposes of
> > > reduction it blocks reduction of its "argument" (it really only
> > > allows substitutions). This would make it possible to write what
> > > you want without needing to introduce names. It also allows you
> > > to eliminate the required phase separation in standard reflective
> > > automation as mentioned by Guillaume (chapter 4, specifically
> > > 4.3, of my dissertation discusses some of these issues as well:
> > > https://gmalecha.github.io/publications/files/malecha-dissertation.pdf).
> > >  
> >
> > I have been having a discussion elsewhere with an Idris developer
> > involved in implementing erasability in Idris (now Idris2).  The new
> > Idris2 erasability binder annotations sound like they could be used
> > in the same way as you describe QUOTE, allowing one to selectively
> > determine which functions can and cannot compute on which arguments.
> > Furthermore, as they are built into Idris2, the language itself can
> > easily take advantage - skipping them completely during
> > computation, not just during extraction.  I wish Coq has something
> > similar, as it would also allow me to drop the erasure axiom
> > (relevant Prop) hack I use elsewhere.
> >  
> I think that QUOTE is a little bit different than erasability in
> general, though it might operate the same way for your purpose.
> Consider, for example, you have a reflective procedure that doesn't
> solve the goal:
> 
> Definition simplify_things (ls : list Prop) : list Prop.
> Theorem simplify_things_ok : forall ls,
>    goalD (simplify_things ls) -> goalD ls.
> 
> You can clearly still phrase this in the standard fully-reflective
> style (as Guillaume suggested):
> 
> Definition rsimplify_things (ls : list term) : list term.
> Theorem simplify_things_ok' : forall (ls ls' : list term),
>   rsimplify_things ls = ls' ->
>   forall mp : instantiation, goalD mp ls' -> goalD mp ls.
> 
> but things are a bit more verbose. Especially, note the (seemingly
> useless) equality proof, which hangs around because we want to use
> [vm_compute] to reduce [rsimplify_things], but we can not use
> [vm_compute] to simplify [goalD] because doing that would destroy the
> structure of our propositions.
> 
> Using QUOTE, you can write the original soundness theorem, and simply
> introduce a QUOTE around every symbol that you want to leave
> uninterpreted.

I think I misunderstood, then.  I thought the point to QUOTE was to
continue to use the proof-carying style instead of the fully-reflective
(Guillaume's) style, but still achieve both the performance benefit and
the modularity (reflective computations cannot attempt to eliminate
atoms from the original goal) that are provided by the fully-reflective
style.

> 
> In your context, you could write
> 
> Theorem reflection_works' : forall (f : Sorted_formula),
>     if solve_sorted f then sfDenote f else True.

Yes.  The attached file does that (although I changed the function name
from "solve_sorted" to "do_reflection" to avoid confusion with the same
named tactic).

Jonathan


(**** [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 Import Coq.Lists.List.
Import ListNotations.

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.

Section Reflect.
  Variable isSingleton : nat -> bool.

  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_skip : Prop -> Sorted_formula. (*unreified props*)

  Fixpoint flatten(lf : List_formula) {struct lf} : 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.

  Definition Known := list (nat * nat).

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

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

   Fixpoint forward_flat(k:Known)(cont:Known->bool)(js:list nat) : bool :=
    match js with
    | nil => (cont k)
    | i::js => forward_flat (add_knowns i k js) cont js
    end.

  Fixpoint forward(k:Known)(cont:Known->bool)(hyp:Sorted_formula){struct hyp} : bool :=
    match hyp with
    | SF_lt i j => cont (add_known i j k)
    | SF_sorted lf => forward_flat k cont (flatten lf)
    | SF_and h1 h2 => forward k (fun k => forward k cont h2) h1
    | SF_or h1 h2 => if forward k cont h1 then forward k cont h2 else false
    | _ => cont k
    end.

  Fixpoint In_part (x:nat*nat)(k:Known) : bool :=
    match k with
    | nil => false
    | y::k' => if natpair_eq_dec x y then true else In_part x k'
    end.

  Fixpoint All_in_part (i:nat)(k:Known)(l:list nat) : bool :=
    match l with
    | nil => true
    | j::l => if In_part (i, j) k then if isSingleton j then true else All_in_part i k l 
              else false
    end.

  Fixpoint In1_part (i:nat)(k:Known) : bool :=
    match k with
    | nil => false
    | (x,y)::k =>
      if (nat_eq_dec x i) then true else
        if (nat_eq_dec y i) then true else
          In1_part i k
    end.

  Fixpoint backward_flat(k:Known)(l:list nat) :=
    match l with
    | nil => true
    | i::nil => if isSingleton i then true else In1_part i k
    | i::l => if All_in_part i k l then backward_flat k l else false
    end.

  Fixpoint backward(k:Known)(f:Sorted_formula){struct f} : bool :=
    match f with
    | SF_lt i j => In_part (i,j) k
    | SF_sorted lf => backward_flat k (flatten lf)
    | SF_and f1 f2 => if backward k f1 then backward k f2 else false
    | SF_or f1 f2 => if backward k f1 then true else backward k f2
    | SF_imp f1 f2 => forward k (fun k => backward k f2) f1
    | SF_skip _ => false
    end.

End Reflect.

Require Export Coq.Classes.RelationClasses.

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

Require Export Coq.Sorting.Sorted.

Notation sorted := (LocallySorted lt).

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

Section defs.
  Context {A : Set}.
  Context {ordA : Ordered A}.
  
  Inductive Atom := Aatom(_:A) | Latom(_:list A).
  Variable atomics : list Atom.
  
  Definition aDenote i : list A :=
    match (nth i atomics (Latom nil)) with
    | Aatom a => [a]
    | Latom l => l
    end.
  
  Definition isSingleton i : bool :=
    match (nth i atomics (Latom nil)) with
    | Aatom _ => true
    | Latom _ => false
    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.

  Fixpoint fDenote(l: list nat) : list A :=
    match l with
    | nil => nil
    | i::l => aDenote i ++ fDenote l
    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 (aDenote i), (aDenote j) with
      | [a], [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_skip p => p
    end.

  (*lemmas showing that flattening is correct*)
  
  Lemma flatten_app : forall l1 l2, fDenote (l1++l2) = fDenote l1 ++ fDenote l2.
  Proof.
    induction l1. intros. simpl.
    - reflexivity.
    - rewrite <-app_assoc. congruence.
  Qed.

  Lemma flatten_correct: forall lf, lfDenote lf = fDenote (flatten lf).
  Proof.
    induction lf. simpl.
    - reflexivity.
    - congruence.
    - apply app_nil_end.
    - rewrite flatten_app. congruence.
  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.

  Fixpoint allOrdered(k:Known) : Prop :=
    match k with
    | nil => True
    | (i, j)::k' => i <# j /\ allOrdered k'
    end.
  
  Lemma in_allOrdered : forall k i j, In (i, j) k -> allOrdered k -> i <# j.
  Proof.
    induction k as [|a k IHk]. intros i j.
    - simpl. contradiction.
    - simpl. intros [->|].
      + tauto.
      + intros. destruct a. apply IHk. tauto.
  Qed.

  Lemma In1_works: forall k n, allOrdered k -> In1_part n k = true -> sorted (aDenote n).
  Proof.
    induction k as [|a k IHk]. intros n H1 H2. simpl in *. 1:discriminate.
    destruct a as [i j]. destruct (nat_eq_dec i n).
    - subst. destruct H1 as (H1 & H0). unfold orderedAtoms in H1. apply (sortedl H1).
    - destruct (nat_eq_dec j n).
      + subst. destruct H1 as (H1 & H0). unfold orderedAtoms in H1. apply (sortedr H1).
      + apply IHk. tauto.
  Qed.

  Lemma All_in_cons: forall i k a l,
      All_in_part isSingleton i k (a::l) = true -> isSingleton a = false ->
      All_in_part isSingleton i k l = true.
  Proof.
    intros i k a l H. simpl in H. destruct (In_part(i, _)) eqn:E1. 2:discriminate.
    destruct (isSingleton a) eqn:E2. 2:congruence. discriminate.
  Qed.

  Lemma InpartIn: forall (k:Known)(x:nat*nat), In_part x k = true -> In x k.
  Proof.
    induction k as [|a k IHk]. intros x H.
    - simpl in H. discriminate.
    - simpl in *. destruct (natpair_eq_dec x a).
      + subst. tauto.
      + right. apply IHk. assumption.
  Qed.

  Lemma All_in_head: forall i k j l,
      allOrdered k -> All_in_part isSingleton i k (j :: l) = true -> i <# j.
  Proof.
    intros i k j l H1 H2.
    simpl in H2. destruct (In_part (i, j) k) eqn:E. 2:discriminate.
    apply InpartIn in E. apply (in_allOrdered k). assumption.
  Qed.

  Lemma flatten_nil : forall l, flatten l = nil -> lfDenote l = nil.
  Proof.
    induction l as [| | |l1 IHl1 l2 IHl2]. intro H. simpl in *.
    - reflexivity.
    - discriminate.
    - discriminate.
    - apply app_eq_nil in H as (H1 & H2).
      rewrite (IHl1 H1), (IHl2 H2). simpl. reflexivity.
  Qed.

  Lemma fDenote_eq: forall i l, aDenote i ++ fDenote l = fDenote (i :: l).
  Proof.
    intros. simpl. reflexivity.
  Qed.

  Lemma sorted_push_singl: forall l k i j,
      allOrdered k ->  All_in_part isSingleton i k (j :: l) = true ->
      sorted (aDenote j ++ fDenote l) -> isSingleton j = true ->
      sorted (aDenote i ++ aDenote j ++ fDenote l).
  Proof.
    intros l k i j H1 H2 H3 H4.
    apply All_in_head in H2. 2:assumption.
    unfold isSingleton in *. unfold orderedAtoms in H2.
    unfold aDenote in H2 at 2. unfold aDenote in H3. unfold aDenote at 2.
    destruct (nth j atomics _) eqn:Ej. 2:discriminate.
    simpl in *. apply sortcomb. assumption.
  Qed.

  Lemma sorted_push: forall l k i j,
      allOrdered k -> All_in_part isSingleton i k (j :: l) = true ->
      sorted (fDenote (j :: l)) -> sorted (aDenote i ++ fDenote (j :: l)).
  Proof.
    induction l as [ |b l IHl]. intros k i j H1 H2 H3.
    - apply All_in_head in H2. 2:assumption.
      simpl. rewrite app_nil_r. assumption.
    - rewrite <-fDenote_eq in *.
      destruct (isSingleton j) eqn:E.
      * apply (sorted_push_singl _ k). assumption.
      * apply All_in_head in H2 as H4. 2:assumption.
        apply All_in_cons in H2. 2:assumption.
        pose proof (IHl k i b H1 H2 (sortedr H3)).
        apply sorted3way. assumption.
  Qed.

  Lemma backward_flat_works: forall l k,
      allOrdered k -> backward_flat isSingleton k l = true -> sorted (fDenote l).
  Proof.
    induction l as [|a l IHl]. intros k H1 H2.
    - constructor.
    - simpl in H2. destruct l.
      + simpl. rewrite app_nil_r.
        destruct (isSingleton a) eqn:E.
        * unfold isSingleton in E.
          unfold aDenote.
          destruct (nth a atomics _).
          -- constructor.
          -- discriminate.
        * apply In1_works in H2. assumption.
      + destruct (All_in_part isSingleton a k (_::l)) eqn:E. 2:discriminate.
        pose proof (IHl k H1 H2) as H3.
        rewrite <-fDenote_eq.
        apply (sorted_push l k _ _ H1 E H3).
  Qed.

  Lemma allOrdered_adds: forall i js k,
      allOrdered k -> sorted (fDenote (i::js)) -> allOrdered (add_knowns i k js).
  Proof.
    induction js as [|a js IHjs]. intros k H1 H2. simpl.
    - assumption.
    - apply IHjs.
      + simpl. intuition idtac.
        simpl in H2. rewrite app_assoc in H2. apply (sortedl H2).
      + simpl in *. apply (sortedm H2).
  Qed.

  Lemma forward_flat_continues: forall l k c,
      allOrdered k -> sorted (fDenote l) -> forward_flat k c l = true ->
      exists k' : Known, allOrdered k' /\ c k' = true.
  Proof.
    induction l as [|a l IHl]. intros k c H1 H2 H3. 
    - exists k. tauto.
    - simpl in H3. refine (IHl _ _ _ _ H3).
      + apply (allOrdered_adds _ _ _ H1 H2).
      + simpl in H2. apply (sortedr H2).
  Qed.

  Lemma forward_continues: forall f k c,
      allOrdered k -> sfDenote f -> forward k c f = true ->
      exists k', allOrdered k' /\ c k' = true.
  Proof.
    induction f as [i j|l|f1 IHf1 f2 IHf2|f1 IHf1 f2 IHf2| |]. intros k c H1 H2 H3.
    simpl in *.
    - exists (add_known i j k). simpl. intuition idtac.
      destruct (aDenote i) as [|? []] eqn:Ei. try assumption.
      destruct (aDenote j) as [|? []] eqn:Ej. try assumption.
      unfold orderedAtoms. rewrite Ei, Ej.
      repeat constructor. assumption.
    - refine (forward_flat_continues (flatten l) k c H1 _ H3).
      rewrite flatten_correct in H2. exact H2.
    - destruct H2 as (Hf1 & Hf2).
      pose proof (IHf1 _ _ H1 Hf1 H3) as [k' (H1' & H3')].
      refine (IHf2 _ _ _ _ H3'). assumption.
    - case_eq (forward k c f1). intro H4. rewrite H4 in H3. 2:discriminate.
      destruct H2 as [H2|H2].
      + apply (IHf1 _ _ H1 H2 H4).
      + apply (IHf2 _ _ H1 H2 H3).
    - exists k. tauto.
    - exists k. tauto.
  Qed.

  Fixpoint reflection_works f k:
    allOrdered k -> backward isSingleton k f = true -> sfDenote f.
  Proof.
    destruct f as [i j|l|f1 f2|f1 f2| |]. simpl. intros X H.
    - apply InpartIn in H. apply in_allOrdered in H. 2:assumption.
      destruct (aDenote i) as [|? []] eqn:Ei. try assumption.
      destruct (aDenote j) as [|? []] eqn:Ej. try assumption.
      unfold orderedAtoms in H.  rewrite Ei, Ej in H.
      simpl in H. inversion H. assumption.
    - rewrite flatten_correct. eapply backward_flat_works. eassumption.
    - destruct (backward isSingleton k f1) eqn:E. 2:discriminate. firstorder.
    - destruct (backward isSingleton k f1) eqn:E. firstorder.
    - intro H1. apply forward_continues in H as [k' (H2 & H3)]. firstorder.
    - discriminate.
  Qed.

  Lemma do_reflection: forall f, if backward isSingleton [] f
                                 then sfDenote f
                                 else True.
  Proof.
    intro f. destruct (backward _ [] f) eqn:E. 2:exact I.
    refine (reflection_works _ _ _ E).
    simpl. exact I.
  Qed.
End defs.

(*Reification tactics*)

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

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

Ltac addToList A x xs :=
  match type of x with
  | A => let b := inList constr:(Aatom x) xs in
         match b with
         | true => xs
         | false => constr:(Aatom x::xs)
         end
  | list A => let b := inList constr:(Latom x) xs in
              match b with
              | true => xs
              | false => constr:(Latom x::xs)
              end
  | _ => xs
  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 constr:(Aatom a) xs in
    let lf := reifyList xs t in
    constr:(LF_cons i lf)
  | ?v =>
    let i := lookup constr:(Latom 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 constr:(Aatom a) xs in
      let nb := lookup constr:(Aatom 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 (do_reflection 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.
    time 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.

  (*This is no longer slow!*)
  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.

  (*This fails because there are no knows to record from the hyp, since all knowns are currently relationships between two atoms.  It should be easy to fix.*)
  Lemma degenerate: forall l, sorted l -> sorted l.
  Proof.
    Fail solve_sorted.
  Abort.
End Examples.