The Coq mailing list

[CREGUT Pierre FTRD/DTL/LAN <pierre.cregut AT rd.francetelecom.fr>]

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.

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.

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)...

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

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

Pierre Crégut

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

PS2> If there is a much clever way to do complex case analysis, let me know !

==========================================================================
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; Auto; Try '(Simplify ())
  | _ -> Fail
And Simplify () :=
  Match Context With [|- ?1] -> '(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 ()); Apply plus_assoc_r.

-- 
Pierre Cregut - 
pierre.cregut AT rd.francetelecom.fr
 - +33 2 96 05 16 28
FTR&D - DTL/MSV - 2 avenue Pierre Marzin - 22307 Lannion Cedex - France