(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* $Id: *)

Require Export Equality.

Declare ML Module "Inv" "Leminv".

Syntax tactic level 0:
| inversion    [<<(Inv $ic $id)>>] -> [ (INVCOM $ic) [1 1] $id]
| inversion_in [<<(InvIn $ic $id ($LIST $l))>>]
    -> [ (INVCOM $ic) [1 1] $id (CLAUSE ($LIST $l))]

| dep_inv [<<(DInv $ic $id)>>] -> ["Dependent " (INVCOM $ic) [1 1] $id]
| dep_inv_with [<<(DInvWith $ic $id $c)>>]
    -> ["Dependent " (INVCOM $ic) [1 1] $id [1 1] "with " $c]

(* Use rules *)

| inv_using
    [<<(UseInversionLemma $id $c)>>] -> ["Inversion " $id [1 1] "using " $c]
| inv_using_in [<<(UseInversionLemmaIn $id $c ($LIST $l))>>]
    -> ["Inversion " $id [1 1] "using " $c (CLAUSE ($LIST $l))]

| simple_inv       [<<(INVCOM "HalfInversion")>>] -> [ "Simple Inversion" ]
| inversion_com    [<<(INVCOM "Inversion")>>] -> [ "Inversion" ]
| inversion_clear  [<<(INVCOM "InversionClear")>>] -> [ "Inversion_clear" ].


Grammar tactic simple_tactic: ast :=
  inversion    [ inversion_com($ic) identarg($id) ] -> [(Inv $ic $id)]
| inversion_num [ inversion_com($ic) pure_numarg($n) ] -> [(Inv $ic $n)]
| inversion_in [ inversion_com($ic) identarg($id) "in" ne_identarg_list($l) ]
      -> [(InvIn $ic $id ($LIST $l))]
| dep_inv   [ "Dependent" inversion_com($ic) identarg($id)] -> [(DInv $ic $id)]
| dep_inv_num  [ "Dependent" inversion_com($ic) pure_numarg($n) ] -> [(DInv $ic $n)]
| dep_inv_with
   [ "Dependent" inversion_com($ic) identarg($id) "with" constrarg($c) ]
     -> [(DInvWith $ic $id $c) ]
| dep_inv_num_with
   [ "Dependent" inversion_com($ic) pure_numarg($n) "with" constrarg($c) ]
     -> [(DInvWith $ic $n $c) ]

| inv_using [ inversion_com($ic) identarg($id) "using" constrarg($c) ]
     -> case [$ic] of
          "Inversion" -> [(UseInversionLemma $id $c)]
        esac

| inv_num_using [ inversion_com($ic) pure_numarg($n) "using" constrarg($c) ]
     -> case [$ic] of
          Inversion -> [(UseInversionLemma $n $c)]
        esac

| inv_using_in
   [ inversion_com($ic) identarg($id) "using" constrarg($c)
     "in" ne_identarg_list($l) ]
     -> case [$ic] of
          "Inversion" -> [(UseInversionLemmaIn $id $c ($LIST $l))]
        esac

with inversion_com: ast :=
  simple_inv    [ "Simple" "Inversion" ] -> [ "HalfInversion" ]
| inversion_com [ "Inversion" ] -> [ "Inversion" ]
| inv_clear     [ "Inversion_clear" ] -> [ "InversionClear" ].


Grammar vernac vernac: ast :=
  der_inv_clr [ "Derive" "Inversion_clear"  identarg($na) identarg($id) "." ]
               -> [(MakeInversionLemmaFromHyp 1 $na $id)]

| der_inv_clr_num [ "Derive" "Inversion_clear"
                     numarg($n) identarg($na) identarg($id) "." ]
                   -> [(MakeInversionLemmaFromHyp $n $na $id)]

| der_inv_clr_with_srt [ "Derive" "Inversion_clear"  identarg($na) 
                         "with" constrarg($com) "Sort" sortarg($s) "." ]
                        -> [(MakeInversionLemma $na $com $s)]

| der_inv_clr_with [ "Derive" "Inversion_clear"  identarg($na)
                     "with" constrarg($com) "." ]
                    -> [(MakeInversionLemma $na $com (CONSTR (PROP))) ]

| der_inv_with_srt [ "Derive" "Inversion" identarg($na)
                     "with" constrarg($com) "Sort" sortarg($s) "." ]
                    -> [(MakeSemiInversionLemma $na $com $s)]

| der_inv_with [ "Derive" "Inversion" identarg($na) "with" constrarg($com) "." ]
                -> [(MakeSemiInversionLemma $na $com (CONSTR (PROP)))]

| der_inv [ "Derive" "Inversion" identarg($na) identarg($id) "." ]
           -> [(MakeSemiInversionLemmaFromHyp 1 $na $id)]

| der_inv_num [ "Derive" "Inversion"
                numarg($n) identarg($na) identarg($id) "." ]
               -> [(MakeSemiInversionLemmaFromHyp $n $na $id)]

| der_dep_inv_with_srt [ "Derive" "Dependent" "Inversion" identarg($na) 
                         "with" constrarg($com) "Sort" sortarg($s) "." ]
                  -> [(MakeDependentSemiInversionLemma $na $com $s)]

| der_dep_inv_clr_with_srt
     [ "Derive" "Dependent" "Inversion_clear"  identarg($na) 
       "with" constrarg($com)  "Sort" sortarg($s)"." ]
      -> [(MakeDependentInversionLemma $na $com $s)].