The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 04/02/2015 04:32 AM, Soegtrop, Michael wrote:
> Dear Jonathan,
>
> I am making some use of 8.5 features, so if the 8.5 version has a cleaner 
> result, I would use the 8.5 version. But I am also curious to see how you 
> solved it in 8.4.
>
> Regarding context searches: I am interested in proof automation performance 
> and context searches with unspecific search patterns and heavy follow up 
> tactics have a bad impact on performance. But context searches with 
> restrictive patterns or lightweight follow up tactics or properly gated 
> heavier tactics are fine. On the other hand everything which leads to good 
> search tree pruning or more stable proof search is usually worth the effort. 
> What counts is ease of use, stability and the final performance. I am quite 
> pragmatic in reaching these goals.

In that case, I have attached the 8.5 version.  Roughly - the 8.4 
version uses refine instead of tactic-in-term to build constrs out of 
tactics - as the "collect_things" technique used in these tactics 
requires a constr to be built that contains the inductive type's match 
expression.  However, the alternate evar-based mechanism I referred to 
would perhaps also work in 8.4, but not as easily (I don't have an 8.4 
version of Coq available to test - so I am saying this based only on 
faulty memory).  That evar-based mechanism avoids the context searches 
by directly building a "list" of the constructor names by selective 
instantiation of an evar, and avoiding the need for context searching a 
constr - hence no need for the constr.

I see below that you are not using tactic-in-terms - favoring instead 
asserts - to test conditions.  Note that asserts, like refines and 
anything else other than tactic-in-term - add to the ongoing proof 
term.  Which you can see at any point in a proof by the command "Show 
Proof".  If you call IsInductiveType successfully many times during a 
single proof, the result will be that the proof term will have one 
unused function/arg (in the case of assert) for every such successful 
call.  All of these would reduce out via beta reduction - but just be 
warned if you ever unfold such a proof before doing any beta reduction 
on it that it will be a mess. Enhancement request 4112 is about this.

Here is what IsInductiveType would look like with tactic-in-term instead 
of assert:

Ltac IsInductiveType type :=
  let unused:=constr:($(
                        let val:=fresh in
                        intro val;
                        destruct val;
                        exact I)$ : (type -> True)) in idtac.

Note also the "let val:=fresh" - else there is a risk of a name clash.

-- Jonathan

> For the time being I think I will go with Ltac as far as possible. Meanwhile 
> I am quite happy with it. I try to delay plugin development until sometime 
> later when my project grows larger.
>
> Here is the final "IsLiteralTerm" tactic which is based on your is_ctor 
> tactic (called IsCtorSym below).
>
> (* Check if the given term is an inductive type *)
>
> Ltac IsInductiveType type :=
>    let H:=fresh in
>    (* Using type as a precondition allows us to get a value of the type 
> during the proof of the assert *)
>    assert (type -> True) as H by (
>      (* val is a opaque value of type 'type' *)
>      intros val;
>      (* See if val can be destructed, if so solve the goal *)
>      destruct val; exact I
>    );
>    (* clear the hypothesis generated by the assert *)
>    clear H.
>
> (* Check if a complete term contains only constructors and inductive type 
> names like a polymorphic list type argument.
>     This includes numbers, lists of numbers, strings, booleans, ... *)
>
> Ltac IsLiteralTerm term := lazymatch term with
> | ?H ?A1 =>
>      (* Debug idtac "f2" H A1; *)
>      IsLiteralTerm H;
>      IsLiteralTerm A1
> | ?H =>
>      (* Debug idtac "f1" H; *)
>      first [ IsCtorSym H | IsInductiveType H ]
> end.
>
> Best regards,
>
> Michael

(*A problem with option (Some, None) is that it is in Type, and so is
restricted in ways that inductives in Prop would not be.  For example,
the term "Some (@Some)" does not type check.  Even if it did work -
being in Type instead of Prop - it would possibly impact extraction,
depending on where it is used.  So, instead of using option, we use
"thing" below (note that "Something (@Something)" does type check).
Since the intent of "thing" is that instances are parsed via Ltac
matches, having it in Prop is not restrictive:*)
Inductive thing : Prop := 
| Something{T}(x:T)
| Nothing.

(*Collect all X's that appear as [Something X] anywhere within the
term (failing when an X is under binders) into a single [Something
X-tuple], or Nothing if there are no [Something X]'s:*)
Ltac collect_things term :=
  let rec f t s :=
      lazymatch t with
      | context C[Something ?S] =>
        (*replace found Something with Nothing so it isn't found
        again*)
        let t':=context C[Nothing] in
        (*Either continue the existing Something tuple s, or start one
        if s is Nothing*)
        lazymatch s with
        | Something ?Ss => f t' (Something (Ss, S))
        | Nothing => f t' (Something S)
        end
      | context [Something] =>
        (*if this pattern matches when the above one doesn't, then
          that must mean that the arg is trapped under binders - which
          the caller should have prevented*)
        fail "collect_things: Something is under binders in" t
      | _ => s
      end in
  f term Nothing.

(*A quick test for the existence of Something x in term - as with
collect_things, this does not work when x is under binders - but
unlike with collect_things, this does not take the time to check for
such problems (which shouldn't exist if the caller has done its
job):*)
Ltac has_something x term :=
  lazymatch term with context [Something x] => idtac end.

Ltac head_of term :=
  lazymatch term with
  | ?H _ => head_of H
  | _ => term
  end.

(*The opposite of "head_of" - return an elaborated version of the
constr term with as many of its args filled in by tac as possible:*)
Ltac elaborate term tac :=
  (*Use "match I with" (the discriminee doesn't matter) as a constr
  version of "first":*)
  match I with
  | _ => elaborate (term $(tac)$) tac
  | _ => term
  end.

(*If the hypothesis H has a value (body), return it unreduced, else
fail.  Uses delta-only reduction restricted to H itself to prevent
further reduction.  Note that if H is a fixpoint, cbv won't unfold it
further - so this reduction is restricted to removing the outermost H
only, which is just what we want:*)
Ltac get_value H := eval cbv delta [H] in H.

Local Definition Quodlibet := forall T, T.

(*Use a "magical sandbox" to find the constructors of an inductive
type.  The sandbox (within a tactic-in-term) is provided with an
instance of Quodlibet (Q) - which can be used to instantiate any type.
The argument tac takes two args: Q and a fresh hypothesis name H - tac
must pose as H an instance of the targeted inductive type, using Q as
needed to fill in any arguments.  The constr that ctors_internal
returns is a function term containing only a match expression with
Something c in each branch for all constructor symbols c:*)
Local Ltac ctors_internal tac :=
  (*reduce the resulting constr - both to get around bugs like 4165,
  and to make searching it faster*)
  eval cbv in
    ($(let Q:=fresh in
       intro Q; (*Q : Quodlibet - for filling any holes*)
       let H:=fresh in
       tac Q H; (*must pose discriminee as H, using Q*)
       let H2:=fresh in
       pose H as H2; (*keep a copy to examine after destructing*)
       tryif destruct H then idtac
       else (let t:=type of H in
             let th:=head_of t in
             fail "ctors_internal:" th "is not an inductive type");
       (*After the destruct of H, H2 in each branch (subgoal) will be
       the constructed instance - with a constructor symbol at its
       head:*)
       let C:=get_value H2 in
       let c:=head_of C in 
       exact (Something c))$ : Quodlibet -> thing).

(*sym is tested to see if it is the head symbol of a constructor of an
inductive type*)
Ltac is_ctor sym :=
  let tac Q H :=
      (*use Q to fill in any args sym might have:*)
      let sym':=elaborate sym ltac:(apply Q) in
      tryif pose sym' as H then idtac
      else fail "is_ctor:" sym "is not even a valid term" in
  let C:=ctors_internal tac in
  (*search for "Something sym" in C:*)
  tryif has_something sym C then idtac
  else fail "is_ctor:" sym "is not a constructor symbol".

(*Return a constr that is either "Something [tuple of constructor
symbols of type]" or "Nothing" if type is inductive but has no
constructors (as with False). *)
Ltac ctors type :=
  let tac Q H := 
      let type':=elaborate type ltac:(apply Q) in
      tryif assert type' as H by apply Q then idtac
      else fail "ctors:" type "is not a valid type" in
  let C:=ctors_internal tac in
  collect_things C.

(*Like ctors, but be permissive about x - it can be anything that can
be elaborated into an inductive type:*)
Ltac ctors' x :=
  (*Allow x it to be:
    - an inductive type (nat)
    - a term of an inductive type (42)
    - a function returning an inductive type (list)
    - a type of a function returning an inductive type (bool->nat)
    - a function returning a term of an inductive type (fun x => x+1)
    - a function returning a type of a - ah - you get the idea
  *)
  let tac Q H := 
      let x':=elaborate x ltac:(apply Q) in
      first [ assert x' as H by apply Q
            | let tx:=type of x' in
              assert tx as H by apply Q
            | fail 1 "ctors':" x "is not a valid type or term"];
      repeat specialize (H (Q _)) in
  let C:=ctors_internal tac in
  collect_things C.

(************************************************************************)
(*Some tests*)

Inductive Weird : nat -> Set :=
| weird0 : Weird 0
| weird1(b : bool) : Weird 1
| weird2(n : nat) : Weird (n - 2)
| weird3(n : nat)(w : Weird (S n)) : n > 2 -> Weird n.

Inductive Strange(x: nat)(w : Weird x) : Set := 
| strange0
| strange1 (b:bool).

Variable T:Type.
Variable F:T.
Variable G:nat.

Record rec : Set := {recfield : nat }.
Record rec2(n : nat) : Type := makerec2 { }.

Goal True.
let x:=ctors rec in idtac x.
is_ctor Build_rec.
let x:=ctors rec2 in idtac x.
is_ctor makerec2.
let x:=ctors' nat in idtac x.
let x:=ctors' 0 in idtac x.
let x:=ctors' (fun t:Type => (forall b:bool, list t)) in idtac x.
let x:=ctors' (fun x => x+2) in idtac x.
let x:=ctors' {|recfield := 0|} in idtac x.
Fail is_ctor F.
Fail ctors T.
Fail ctors F.
Fail is_ctor G.
is_ctor @None.
is_ctor Some.
is_ctor @eq_refl.
let x:=ctors @eq in idtac x.
let x:=ctors @prod in idtac x.
is_ctor @pair.
let x:=ctors option in idtac x.
let x:=ctors thing in idtac x.
let x:=ctors False in idtac x.
let x:=ctors bool in idtac x.
let x:=ctors list in idtac x.
is_ctor cons.
is_ctor 0.
Fail is_ctor (@cons nat).
is_ctor @cons.
is_ctor S.
Fail is_ctor (cons 1 nil).
Fail is_ctor 1.
Fail is_ctor X.
let x:=ctors (list nat) in idtac x.
let x:=ctors nat in idtac x.
let x:=ctors Weird in idtac x.
is_ctor weird3.
let x:=ctors Strange in idtac x.
exact I.
Show Proof.
Qed.