Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Automatic finding false hypothesis

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Automatic finding false hypothesis


chronological Thread 
  • From: Marko Malikovi� <marko AT ffri.hr>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] Automatic finding false hypothesis
  • Date: Sat, 24 Nov 2007 16:42:25 +0100 (CET)
  • Importance: Normal
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Greetings,

is there some another tactic (except "omega") which can automatically find
false hypothesis in form of inequality and solve the goal, for example:

Hyp1 : 5>6

I know just ident of hypothesis ("Hyp1") but not his statement (we don't
know is it 5>6 or 100<=50). So, "absurd" tactic is not enough.

If it is just a "omega" tactic, can somebody explain me this error:

User error: Omega: Unrecognized atomic proposition: my_proposition

Thank you very much,

Marko Malikoviæ





Archive powered by MhonArc 2.6.16.

Top of Page