The Coq mailing list

[David Delahaye <delahaye AT jurancon.inria.fr>]

    Hi Pierre,

> I have a few questions on LTAC :
> 
> What is the syntax for tactic without arguments :
> files say Tactic Definition foo :=
> but Tactic Definition foo := Match Context With .... generates an error.
> I cannot call '(foo ()) because it complains on () and '(foo) does not work.
> If I try '(foo O) it complains about foo being an unknown reference...
> 
> I have a "no matching clauses for Match Context" when i try to inline
> Simplify (call to loop but without recursive call to simplify). There is 
> a default case in loop and Simplify just matches the goal.

    Several things here:

    - Match Context is not a value of LTAC and it requires a proof context to
      be evaluated (a goal actually). When you make a toplevel definition, you
      are not under a proof context and if you use directly Match Context then
      it complains because it wants a goal. To avoid that, you have to use a
      closure using (). May be, I will change this in the final release by
      considering Match Context directly as a closure.

    - There was a very recent change of syntax for application in LTAC (so 
that
      the small documentation is not updated, sorry for that) which is not
      quoted anymore. So you can directly write (foo ()). But now, you have to
      quote applications of Coq's terms, e.g., (bar '(S O)) where bar is a
      toplevel definition.

> There is an underlying assumption in the use of pattern in LTAC that any
> term of constr can be decomposed with a pattern because patterns are just
> terms with holes.  But it is not clear to me how I can match a Case.
> Can I just type Case ?1 of end to catch
> - the fact the term is a case
> - the term on which a case analysis is done.

    No, it's not enough. You have to provide also the number of patterns in 
the
Case. Here, in your case, (Case ?1 of ? ? end) will make the job. I give you
back, in attachment, your test example modified to work properly with the
release.

> While I was trying to understand the PermutProve example,
> I noticed that Eval ... in is more or less at the construction level.
> But if I write Definition x := Eval Compute in (plus (1) (1)). 
> x is still (plus (1) (1)). But Eval Compute in (plus (1) (1)) replies (2)...

    Well, this means that Definition doesn't make its job. It is now fixed.
Thank you.

> Why is Match not closed as other case constructs in Coq ?
> Match with end is still in the Coq syntax...

    Match and Match Context belong to the metalanguage world. So, I don't 
think
we have to use a syntax based on Coq's one because the two languages are not 
at
the same level and we have to distinguish them from each other. These two
structures have a syntax similar to Ocaml's one, the big metalanguage, and it
seems to be more intuitive.

> I have added the test example I would have liked to write. 
> What is wrong with it ?

    I give you the modifications. The problems were the quotes, the Case and
some other non-significant details.

> Pierre Crégut
> 
> PS> The Field example cited in the Delahaye and Mayero paper does not work
> with this beta release.

    Well, it's due to a syntactical change (the quote) in LTAC. We have a
correct version which works well and we're going to make it available by FTP.

    David.

===============================================================================
David Delahaye                                 <Email>: 
David.Delahaye AT inria.fr
<Laboratory>: The Coq Project                                  <Domain>: 
Proofs
<Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
          FRANCE
<Tel>: (33)-(0)1 39 63 57 53
<Fax>: (33)-(0)1 39 63 56 84
<Url>: http://pauillac.inria.fr/~delahaye
===============================================================================

[If you have time to waste, you can have a look on my proof that 2 = 1. We 
know
 that, for -1 < x <= 1:

   ln(1 + x) = x - 1/2(x^2) + 1/3(x^3) - 1/4(x^4) + ...

 Let x = 1:

   ln(2) = 1 - 1/2 + 1/3 - 1/4 + 1/5 - 1/6 + 1/7 - 1/8 + 1/9 - ...

 Let multiply the two members by 2:

   2ln(2) = 2 - 2/2 + 2/3 - 2/4 + 2/5 - 2/6 + 2/7 - 2/8 + 2/9 - ...
   2ln(2) = 2 - 1 + 2/3 - 1/2 + 2/5 - 1/3 + 2/7 - 1/4 + 2/9 - ...

 Let sum the terms with the same denominator:

   2ln(2) = 1 - 1/2 + 1/3 - 1/4 + 1/5 - 1/6 + 1/7 - ...
   2ln(2) = ln(2)

 Finally, 2 = 1.]
Require Arith.

Inductive term: Set := Tplus : term -> term -> term | Tnat : nat -> term.

Fixpoint interp [t: term] : nat := 
  Cases t of 
    (Tplus t1 t2) => (plus (interp t1) (interp t2))
  | (Tnat n) => n
  end.

Recursive Tactic Definition loop t :=
  Match t With
    [(Tplus ?1 ?2)] -> (loop ?1) Orelse (loop ?2)
  | [(Case ?1 of ? ? end)] -> Case ?1; Intros; Auto; (Simplify ())
  | _ -> Fail
And Simplify () :=
  Match Context With [|- ? = (interp ?1)] -> Try (loop ?1).

Definition stable [f: term -> term] := (x: term) (interp x) = (interp (f x)).

Definition assoc [t: term] :=
  Cases t of (Tplus (Tplus x y) z) => (Tplus x (Tplus y z)) | _ => t  end.

Theorem assoc_stable : (stable assoc).

Unfold stable assoc; Intro x; (Simplify ()); Simpl; Apply plus_assoc_r.