Quelle  ltac.v   Sprache: Coq

(* The tactic language *)

(* Submitted by Pierre Crégut *)
(* Checks substitution of x *)
Ltac f x := unfold x; idtac.

Lemma lem1 : 0 + 0 = 0.
f plus.
reflexivity.
Qed.

(* Submitted by Pierre Crégut *)
(* Check syntactic correctness *)
Ltac F x := idtac; G x
 with G y := idtac; F y.

(* Check that Match Context keeps a closure *)
Ltac U := let a := constr:(I) in
          match goal with
          |  |- _ => apply a
          end.

Lemma lem2 : True.
U.
Qed.

(* Check that Match giving non-tactic arguments are evaluated at Let-time *)

Ltac B := let y := (match goal with
                    | z:_ |- _ => z
                    end) in
          (intro H1; exact y).

Lemma lem3 : True -> False -> True -> False.
intros H H0.
B.  (* y is H0 if at let-time, H1 otherwise *)
Qed.

(* Checks the matching order of hypotheses *)
Ltac Y := match goal with
          | x:_,y:_ |- _ => apply x
          end.
Ltac Z := match goal with
          | y:_,x:_ |- _ => apply x
          end.

Lemma lem4 : (True -> False) -> (False -> False) -> False.
intros H H0.
Z. (* Apply H0 *)
Y. (* Apply H *)
exact I.
Qed.

(* Check backtracking *)
Lemma back1 : 0 = 1 -> 0 = 0 -> 1 = 1 -> 0 = 0.
intros;
 match goal with
 | _:(0 = ?X1),_:(1 = 1) |- _ => exact (refl_equal X1)
 end.
Qed.

Lemma back2 : 0 = 0 -> 0 = 1 -> 1 = 1 -> 0 = 0.
intros;
 match goal with
 | _:(0 = ?X1),_:(1 = 1) |- _ => exact (refl_equal X1)
 end.
Qed.

Lemma back3 : 0 = 0 -> 1 = 1 -> 0 = 1 -> 0 = 0.
intros;
 match goal with
 | _:(0 = ?X1),_:(1 = 1) |- _ => exact (refl_equal X1)
 end.
Qed.

(* Check context binding *)
Ltac sym t :=
  match constr:(t) with
  | context C[(?X1 = ?X2)] => context C [X1 = X2]
  end.

Lemma sym : 0 <> 1 -> 1 <> 0.
intro H.
let t := sym type of H in
assert t.
exact H.
intro H1.
apply H.
symmetry .
assumption.
Qed.

(* Check context binding in match goal *)
(* This wasn't working in V8.0pl1, as the list of matched hyps wasn't empty *)
Ltac sym' :=
  match goal with
  | _:True |- context C[(?X1 = ?X2)] =>
      let t := context C [X2 = X1] in
      assert t
  end.

Lemma sym' : True -> 0 <> 1 -> 1 <> 0.
intros Ht H.
sym'.
exact H.
intro H1.
apply H.
symmetry .
assumption.
Qed.

(* Check that fails abort the current match context *)
Lemma decide : True \/ False.
match goal with
| _ => fail 1
| _ => right
end || left.
exact I.
Qed.

(* Check that "match c with" backtracks on subterms *)
Lemma refl : 1 = 1.
let t :=
 (match constr:(1 = 2) with
  | context [(S ?X1)] => constr:(refl_equal X1:1 = 1)
  end) in
assert (H := t).
assumption.
Qed.

(* Note that backtracking in "match c with" is only on type-checking not on
evaluation of tactics. E.g., this does not work

Lemma refl : (1)=(1).
Match (1)=(2) With
  [[(S ?1)]] -> Apply (refl_equal nat ?1).
Qed.
*)


(* Check the precedences of rel context, ltac context and vars context *)
(* (was wrong in V8.0) *)

Ltac check_binding y := cut ((fun y => y) = S).
Goal True.
check_binding ipattern:(H).
Abort.

(* Check that variables explicitly parsed as ltac variables are not
   seen as intro pattern or constr (BZ#984) *)

Ltac afi tac := intros; tac.
Goal 1 = 2.
afi ltac:(auto).
Abort.

(* Tactic Notation avec listes *)

Tactic Notation "pat" hyp(id) "occs" integer_list(l) := pattern id at l.

Goal forall x, x=0 -> x=x.
intro x.
pat x occs 1 3.
Abort.

Tactic Notation "revert" ne_hyp_list(l) := generalize l; clear l.

Goal forall a b c, a=0 -> b=c+a.
intros.
revert a b c H.
Abort.

(* Used to fail until revision 9280 because of a parasitic App node with
   empty args *)

Goal True.
match constr:(@None) with @None => exact I end.
Abort.

(* Check second-order pattern unification *)

Ltac to_exist :=
  match goal with
  |- forall x y, @?P x y =>
    let Q := eval lazy beta in (exists x, forall y, P x y) in
    assert (Q->Q)
  end.

Goal forall x y : nat, x = y.
to_exist. exact (fun H => H).
Abort.

(* Used to fail in V8.1 *)

Tactic Notation "test" constr(t) integer(n) :=
   set (k := t) at n.

Goal forall x : nat, x = 1 -> x + x + x = 3.
intros x H.
test x 2.
Abort.

(* Utilisation de let rec sans arguments *)

Ltac is :=
  let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in
  i.

Goal True -> True -> True.
is.
exact I.
Abort.

(* Interférence entre espaces des noms *)

Ltac O := intro.
Ltac Z1 t := set (x:=t).
Ltac Z2 t := t.
Goal True -> True.
Z1 O.
Z2 ltac:(O).
exact I.
Qed.

(* Illegal application used to make Ltac loop. *)

Section LtacLoopTest.
  Ltac g x := idtac.
  Goal True.
  Timeout 1 try g()().
  Abort.
End LtacLoopTest.

(* Test binding of open terms *)

Ltac test_open_match z :=
  match z with
    (forall y x, ?h = 0) => assert (forall x y, h = x + y)
  end.

Goal True.
test_open_match (forall z y, y + z  = 0).
reflexivity.
apply I.
Qed.

(* Test binding of open terms with non linear matching *)

Ltac f_non_linear t :=
  match t with
    (forall x y, ?u = 0) -> (forall y x, ?u = 0) =>
       assert (forall x y:nat, u = u)
  end.

Goal True.
f_non_linear ((forall x y, x+y = 0) -> (forall x y, y+x = 0)).
reflexivity.
f_non_linear ((forall a b, a+b = 0) -> (forall a b, b+a = 0)).
reflexivity.
f_non_linear ((forall a b, a+b = 0) -> (forall x y, y+x = 0)).
reflexivity.
f_non_linear ((forall x y, x+y = 0) -> (forall a b, b+a = 0)).
reflexivity.
f_non_linear ((forall x y, x+y = 0) -> (forall y x, x+y = 0)).
reflexivity.
f_non_linear ((forall x y, x+y = 0) -> (forall y x, y+x = 0)) (* should fail *)
|| exact I.
Qed.

(* Test regular failure when clear/intro breaks soundness of the
   interpretation of terms in current environment *)

Ltac g y := clear y; assert (y=y).
Goal forall x:nat, True.
intro x.
Fail g x.
Abort.

Ltac h y := assert (y=y).
Goal forall x:nat, True.
intro x.
Fail clear x; f x.
Abort.

(* Do not consider evars as unification holes in Ltac matching (and at
   least not as holes unrelated to the original evars)
   [Example adapted from Ynot code]
 *)

Ltac not_eq e1 e2 :=
  match e1 with
    | e2 => fail 1
    | _ => idtac
  end.

Goal True.
evar(foo:nat).
let evval := eval compute in foo in not_eq evval 1.
let evval := eval compute in foo in not_eq 1 evval.
Abort.

(* Check instantiation of binders using ltac names *)

Goal True.
let x := ipattern:(y) in assert (forall x y, x = y + 0).
intro.
destruct y. (* Check that the name is y here *)
Abort.

(* An example suggested by Jason (see #4317) showing the intended semantics *)
(* Order of binders is reverted because y is just told to depend on x *)

Goal 1=1.
let T := constr:(fun a b : nat => a) in
  lazymatch T with
  | (fun x z => ?y) => pose ((fun x x => y) 2 1)
  end.
exact (eq_refl n).
Qed.

(* A variant of #2602 which was wrongly succeeding because "a", bound to
   "?m", was then internally turned into a "_" in the second matching *)

Goal exists m, S m > 0.
eexists.
Fail match goal with
 | |- context [ S ?a ] =>
     match goal with
       | |- S a > a => idtac
     end
end.
Abort.

(* Test evar syntax *)

Goal True.
evar (0=0).
Abort.

(* Test location of hypothesis in "symmetry in H". This was broken in
   8.6 where H, when the oldest hyp, was moved at the place of most
   recent hypothesis *)

Goal 0=1 -> True -> True.
intros H H0.
symmetry in H.
(* H should be the first hypothesis *)
match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *)
exact (eq_refl H0).
Abort.

(* Check that internal names used in "match" compilation to push "term
   to match" on the environment are not interpreted as ltac variables *)

Module ToMatchNames.
Ltac g c := let r := constr:(match c return _ with a => 1 end) in idtac.
Goal True.
g 1.
Abort.
End ToMatchNames.

(* An example where internal names used to build the return predicate
   (here "n" because "a" is bound to "nil" and "n" is the first letter
   of "nil") by small inversion should be taken distinct from Ltac names. *)

Module LtacNames.
Inductive t (A : Type) : nat -> Type :=
    nil : t A 0 | cons : A -> forall n : nat, t A n -> t A (S n).

Ltac f a n :=
  let x := constr:(match a with nil _ => true | cons _ _ _ _ => I end) in
  assert (x=x/\n=n).

Goal forall (y:t nat 0), True.
intros.
f y true.
Abort.

End LtacNames.

(* Test binding of the name of existential variables in Ltac *)

Module EvarNames.

Ltac pick x := eexists ?[x].
Goal exists y, y = 0.
pick foo.
[foo]:exact 0.
auto.
Qed.

Ltac goal x := refine ?[x].

Goal forall n, n + 0 = n.
Proof.
  induction n; [ goal Base | goal Rec ].
  [Base]: {
    easy.
  }
  [Rec]: {
    simpl.
    now f_equal.
  }
Qed.

End EvarNames.

Module LocalRedef.
  Ltac thetac := idtac.
  Ltac thetac' := idtac.

  Module Inner.
    Ltac thetac ::= fail.
    Local Ltac thetac' ::= fail.
    Goal False.
      Fail thetac.
      Fail thetac'.
    Abort.
  End Inner.
  Goal False.
    Fail thetac.
    thetac'.
  Abort.

  Section S.
    Variable f : False.
    Fail Global Ltac thetac' ::= exact f.
    Ltac thetac' ::= exact f.
    Goal False.
    Proof. thetac'. Qed.
  End S.
  Goal False.
  Proof.
    thetac'.
    Fail Qed.
  Abort.
End LocalRedef.

Module MatchCastInPattern.

  Goal let x := True in True.
  Proof.
    intro x.
    lazymatch goal with
    | [ H := ?v : ?T |- _ ] => constr_eq T Prop
    end.

    Fail lazymatch goal with
    | [ H := ?v <: ?T |- _ ] => constr_eq T Prop
    end. (* Warning: Casts are ignored in patterns [cast-in-pattern,automation] *)

    Set Warnings "+cast-in-pattern".
    Fail lazymatch goal with
    | [ H := ?v <: _ |- _ ] => idtac
    end.
    Fail lazymatch goal with
    | [ H := [ ?v : _ ] : _ |- _ ] => idtac
    end.
  Abort.

End MatchCastInPattern.

Module StrictModeConfusion.

Goal True.
Fail let x := constr:(match _ with x x => _ end) in idtac.
(* for_grammar does not reset the ref when an exception is raised *)
Abort.

Fail Ltac bad := exact x. (* was wrongly accepted *)

End StrictModeConfusion.