coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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æ
- [Coq-Club] How to compare hypotheses over subgoals, marko
Archive powered by MhonArc 2.6.16.