The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello, Helge --

Did anyone reply to your question? One way to do this would be to use [fst] instead of pattern matching. You can prove:

Lemma pair_eta : forall {T U} (x : T * U), x = (fst x, snd x).

Proof. destruct x; reflexivity. Defined.

repeat match goal with

       | |- context [ match ?X with (_,_) => _ end ] => rewrite (@pair_eta _ _ X)

       end.

and then phrase your lemmas in terms of [fst], e.g.

forall x, f (fst (baz x)) = g_baz x

Here's an example interaction:

Axiom f : nat -> Prop.

Axiom foo : nat -> nat * nat.

Axiom bar : nat -> nat * nat * nat.

Axiom baz : nat -> nat * nat.

Axiom g_baz : nat -> Prop.

Lemma pair_eta : forall {T U} (x : T * U), x = (fst x, snd x).

Proof. destruct x; reflexivity. Defined.

Axiom f_baz : forall x, f (fst (baz x)) = g_baz x.

Goal forall x,

    f (

    let (x', _) := foo x in

    let '(x'', _, _) := bar x' in

    let (x''', _) := baz x'' in

    x''').

Proof.

  intros.

  repeat match goal with

         | |- context [ match ?X with (_,_) => _ end ] => rewrite (@pair_eta _ _ X)

         end.

  rewrite f_baz.

I hope that this helps.

On Mon, Aug 10, 2015 at 1:18 PM, Helge Bahmann <hcb AT chaoticmind.net> wrote:

Hello all,

I have expressions of the kind:

  f (
    let (x', _) := foo x in
    let (x'', _, _) := bar x' in
    let (x''', _) := baz x'' in
    x''')

which needs to be reduced for a proof, and there are
rules available for performing reduction per each individual
inner operator. There are different ways that I can present these, but
essentially they are all of the kind:

  let (x', _) := baz x in f x' = g_baz (f x)

What I am looking is for ways to automate applications of
these reductions. These need to be performed
"inside out" (first reduce f/baz, then f/bar, then f/foo), but
I always hit a wall trying to formulate the lifting required
in a generalizable fashion.

Does anyone have a trick handy that could apply in a situation
like this? Possibly even automating the case analysis, I already
have trouble with that (given that "foo x"/"bar x"/"baz x" all
have different types and I cannot seem to generalize over that).

Thanks,
Helge

--

gregory malecha