The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

You are right but in coq there is a difference between what the user writes and what coq stores: pattern matching are always compiled into non ambiguous ones (what you call "all different constructor and free variables") because that it is the only form that the calculus of constructions supports. So if you look at terms (*), not user written pre-terms, pattern matching are *always* in this particular form. That said most of the time in proofs we prefer remembering the user written pattern matching. 

P.

(*) preferably with "Set Printing All" because the default term printer tends to de-compile on the fly to make things readable. 

Le mar. 16 août 2022 à 11:24, Vedran Čačić <veky AT math.hr> a écrit :

Well, it is possible that _I_ misunderstood the OP's question. If Form's are actually all the different constructors of a type of h, and all x are actually free variables, and *there is no last case (with Value_others, which you conveniently disregarded;)*, then yes, the equivalence holds. But as soon as any of these assumptions are not met, a counterexample exists.

My remark was that you _can_ save the equivalence, by converting

y1 if P1

y2 if P2

...

yl if Pl

y0 otherwise

not into (as OP suggested)

(P1 /\ y1) \/ (P2 /\ y2) \/ ... \/ (Pl /\ yl) \/ y0

but into (more complicated but models what Coq actually does better)

(P1 /\ y1) \/ (~P1 /\ P2 /\ y2) \/ (~P1 /\ ~P2 /\ P3 /\ y3) \/ ... \/ (~P1 /\ ~P2 /\ ... /\ ~Pl /\ y0).

I hope it is clearer now. Yes, if Pi are actually disjoint (different constructors are an important special case, of course), and there is no "else branch", these are the same, but in general, they are not.

čet, 4. kol 2022. u 09:12 mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> napisao je:

Hi Vedran,

Sorry, I did not get "so each case should have conjoined the negations
of previous ones if you really want equivalence", so could you please
explain? The equivalence holds [1], unless I have misunderstood
Wendlasida's question.

Best,
Mukesh

[1] https://gist.github.com/mukeshtiwari/c2afb95b5f3db39b5cb75e5b4a44e363


Inductive Constructors : Type :=
| First (n : nat)
| Second (n m : nat)
| Third (n m p : nat).


(* The proof can definitely be shorten using Ltac *)
Lemma ex_rewrite :
forall (h : Constructors) opt,
opt = match h with
| First n => n
| Second n m => m
| Third n m p => p
end <->
(exists n, h = First n /\ opt = n) \/
(exists n m, h = Second n m /\ opt = m) \/
(exists n m p, h = Third n m p /\ opt = p).
Proof.
destruct h;
intros ?; split;
intro H.
+ left. eauto.
+ destruct H as [[w [Ha Hb]] | [[w [Ha [Hb Hc]]] |
[w H]]].
++ inversion Ha; subst;
auto.
++ congruence.
++ destruct H as (m & p & Hf & Hw).
congruence.
+ right; left.
eauto.
+ destruct H as [[w [Ha Hb]] | [[w [Ha [Hb Hc]]] |
[w H]]].
++ congruence.
++ inversion Hb; subst; reflexivity.
++ destruct H as (mt & p & Hf & Hw).
congruence.
+ right; right.
eauto.
+ destruct H as [[w [Ha Hb]] | [[w [Ha [Hb Hc]]] |
[w H]]].
++ congruence.
++ congruence.
++ destruct H as (mt & pt & Hf & Hw).
inversion Hf; subst.
reflexivity.
Qed.

On Wed, Aug 3, 2022 at 5:29 PM Vedran Čačić <veky AT math.hr> wrote:
>
> Of course, the lemma can't be <->: patterns are matched from top to bottom, so each case should have conjoined the negations of previous ones if you really want equivalence. However, the -> direction, which OP was interested in, holds.
>
> ~Veky
>
> On Sat, Jul 30, 2022, 15:37 mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:
>>
>> 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

--

Vedran Čačić