coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Eliminate duplicate subgoals?

From: Colm Bhandal <bhandalc AT tcd.ie>
To: coq club <coq-club AT inria.fr>
Subject: [Coq-Club] Eliminate duplicate subgoals?
Date: Fri, 14 Nov 2014 19:14:04 +0000

Hi,

I am wondering if anybody had any idea how to use tactics in Coq to eliminate identical subgoals? More preciselsy, let's say there are two subgoals:

[H1, H2, H3, ... |- SG] and [H1, H2, H3, ... |- SG] in the context such that all the hypotheses and the goals are the same in each case.

It would be nice if there was a tactic "prune" or something to get rid of the duplicate subgoal. Anybody got any ideas how to write a tactic like this or does one already exist maybe?

Thanks,

Colm

[Coq-Club] Eliminate duplicate subgoals?, Colm Bhandal, 11/14/2014
- Re: [Coq-Club] Eliminate duplicate subgoals?, Jonathan, 11/14/2014
  - Re: [Coq-Club] Eliminate duplicate subgoals?, Jason Gross, 11/14/2014
    - Re: [Coq-Club] Eliminate duplicate subgoals?, Jonathan, 11/14/2014
      - Re: [Coq-Club] Eliminate duplicate subgoals?, Jonathan, 11/15/2014
        
        Re: [Coq-Club] Eliminate duplicate subgoals?, Randy Pollack, 11/15/2014
        
        Re: [Coq-Club] Eliminate duplicate subgoals?, Jonathan, 11/15/2014
- Re: [Coq-Club] Eliminate duplicate subgoals?, Enrico Tassi, 11/15/2014
  - Re: [Coq-Club] Eliminate duplicate subgoals?, Pierre-Marie Pédrot, 11/15/2014
    - Re: [Coq-Club] Eliminate duplicate subgoals?, Colm Bhandal, 11/15/2014
      - Re: [Coq-Club] Eliminate duplicate subgoals?, Colm Bhandal, 11/15/2014