Coq - Assign expression to variable

user_3613657 0
Viewed 41

First and foremost, I'm not yet very familiar with Coq lingo, so I will use terms like e.g. 'expression' and 'variable' loosely, but they are probably not the correct Coq terms.

I'm trying to prove the following subgoal of a Theorem.

1 goal
b : bag
v, b' : nat
b'' : natlist
B : b = b' :: b''
IHb'' : b = b'' -> count v (add v b'') = count v b'' + 1
______________________________________(1/1)
S match v =? b' with
  | true => S (count v b'')
  | false => count v b''
  end = match v =? b' with
        | true => S (count v b'')
        | false => count v b''
        end + 1

You can ignore S and + 1, I'm basically looking for a way to assign

match v =? b' with
  | true => S (count v b'')
  | false => count v b''
  end

to a variable of type nat because it occurs on both sides of the equation. How can I do this? Or do I need to go through destroying v and b' and proving all cases separately?

coq
2 Answers

Here are two possibilities. There may well be better ones.

You can use set to give a name to a term. All the occurrences of that term are replaced by the variable.

set (x := match v =? b' with
          | true => S (count v b'')
          | false => count v b''
          end).

Sometimes you need to hide the definition of the variable, and only remember it as an equality that you invoke on demand. For that, use remember.

You can match the goal against a pattern using the context form of match goal and give a name to whatever's inside that pattern.

match goal with |- context [S ?_x = ?_x + 1] => set (x := _x) end.

If this is your real goal and not a simplified example, it's a simple arithmetic statement and you can just call lia and let Coq figure it out.

Require Import Lia.

…
lia.
user_3870760

Besides Gilles's suggestions you can use the ssreflect set to achieve this, in at least two ways illustrated here:

Require Import Arith ssreflect.

Variables v b' b'' : nat.
Variable count : nat -> nat -> nat.

Goal
 S match v =? b' with
   | true => S (count v b'')
   | false => count v b''
   end
 = match v =? b' with
   | true => S (count v b'')
   | false => count v b''
   end + 1.
Proof.
  set t := (X in S X = X + _).
  Undo.
  set t := match _ with true => _ | false => _ end.
Abort.

The latter one also works with the regular set but it needs brackets:

  set (t := match _ with true => _ | false => _ end).
user_23054580
Related