The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon xiang sen 
<xiangsen AT ustc.edu>:

> Hi, all
>
> I want to apply my customized tactic to a specified hypo.
>
> So I do this:
>
> Ltac reverse H :=
> match goal with
> | [ H : ? a < ?b |- _ ] => assert ( b > a); [ omega | clear H]
> end.
>
> I works well when there is only one hypo matching some x < y,
> but if there are several hypo such as H1 : a < b, H2 : x < y,
> "reverse H1" doesn't work as expected.



In your tactic, the second occurrence of H in your tactic is a
pattern variable, which is instantiated by the fresher  hypothesis
it matches.

A solution to this problem can be using "type of"



Ltac reverse1 H :=
match type of H with
 ?a < ?b => assert ( b > a); [ assumption | try (clear H)]
end.


In fact, "H" can be any term whose type is a strict inequality.
Thus I put a "try" before "clear H".

By the way, I did'nt use "omega", since "b>a" and "a>b" are convertible, so
"assumption" is OK.


Lemma try2: 1 < 2 -> 3 < 4 -> 7 <= 9.
intros.
(*
 1 subgoal

  H : 1 < 2
  H0 : 3 < 4
  ============================
   7 <= 9
*)

 reverse1 H.
(*

 1 subgoal

  H0 : 3 < 4
  H1 : 2 > 1
  ============================
   7 <= 9

*)
 Undo.
 reverse1 H0.



(*

1 subgoal

  H : 1 < 2
  H1 : 4 > 3
  ============================
   7 <= 9


*)
Abort.


Cheers,

Pierre


>
> Why and how? Thanks
>
> Best,
> Xiang Sen
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.