The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Wendlasida,

I am not sure that it’s the best way but one way to do is to define a lemma:

Lemma ex_rewrite : forall opt h, 

(opt = match h with
| Form_1 x => Value_1
| Form_2 x1 x2 => Value_2
...
| Form_n x1... xn => Value_n
| _ => Value_others )  <-> 

(exists x, h = Form_1 x /\ opt = Value_1) \/ (exists x1 x2, h = Form_2 x1 x2 /\ opt = Value_1) ... (exists x1 ... xn, h = Form_n x1 xn /\ opt = Value_n) \/ (opt = Value_others).

You prove it once and use it everywhere. (However, if h appears in somewhere in your  proof, then ‘destruct h’ (or case h which you are already doing) would give you all the constructors and you can discharge them accordingly, so I am not sure if the above is going add any value). 

Best,

Mukesh

On Sat, 30 Jul 2022 at 11:26, Wendlasida Ouedraogo <ouedraogo.tertius AT gmail.com> wrote:

Dear All,

I am currently working on programs that perform a lot of pattern matchings. I am looking for a tactic or an existing library that can help me to transform an hypothesis like:

opt = match h with
| Form_1 x => Value_1
| Form_2 x1 x2 => Value_2
...
| Form_n x1... xn => Value_n
| _ => Value_others

into

(exists x, h = Form_1 x /\ opt = Value_1) \/ (exists x1 x2, h = Form_2 x1 x2 /\ opt = Value_1) ... (exists x1 ... xn, h = Form_n x1 xn /\ opt = Value_n) \/ (opt = Value_others)

Is there a tactic that can perform such transformation? I usually perform this transformation using the "assert" and "case" tactics that lead to long proofs or a high number of subgoals. Any ideas?

--

Cordialement,

M. Wendlasida Tertius OUEDRAOGO

Mobile : 0751061208