Skip to Content.
Sympa Menu

coq-club - [Coq-Club] How to compare hypotheses over subgoals

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to compare hypotheses over subgoals


chronological Thread 
  • From: marko AT ffri.hr
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] How to compare hypotheses over subgoals
  • Date: Fri, 28 Mar 2008 16:36:28 +0100 (CET)
  • Importance: Normal
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Greetings,

If I have something like this:

Section Proba.
Inductive elementi1 : Set := a1 | b1 | c1 | d1 | e1 | f1 | g1.
Inductive elementi2 : Set := a2 | b2 | c2 | d2 | e2 | f2 | g2.
Inductive elementi3 : Set := a3 | b3 | c3 | d3 | e3 | f3 | g3.
Inductive elementi4 : Set := a4 | b4 | c4 | d4 | e4 | f4 | g4.
Require Import List.
Parameter predikat : elementi1 -> elementi2 -> elementi3 -> elementi4 ->
Prop.
Parameter lista_predikata : list Prop.
Parameter goal : Prop.
Hypothesis H : lista_predikata = predikat a1 b2 a3 c4 :: predikat d1 c2 a3
c4 :: nil.

Coq < Goal goal.
1 subgoal

  H : lista_predikata = predikat a1 b2 a3 c4 :: predikat d1 c2 a3 c4 :: nil
  ============================
   goal

Unnamed_thm <

and if I have several subgoals but each subgoal contain hypothesis H of
same type and the same lenght but (maybe) with different elements (a1
b2... and so on can be different on different places).

The question is: "How can I compare hypotheses H in different subgoals and
if in each subgoals the hypotheses H are the same then apply some tactic?"

Any idea?

Thank you wery much,

Marko Malikoviæ





Archive powered by MhonArc 2.6.16.

Top of Page