Coq - Assign expression to variable

Question

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 subgoal

  b : bag
  v, b' : nat
  b'' : natlist
  B : b = b' :: b''
  IHb'' : b = b'' ->
          count v (add v b'') = count v b'' + 1
  ============================
  S (if v =? b' then S (count v b'') else count v b'') =
  (if v =? b' then S (count v b'') else count v b'') +
  1

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

if v =? b' then S (count v b'') else count v b''

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?

Answer (Gilles 'SO- stop being evil')

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 := if v =? b' then S (count v b'') else count v b'').
b: bag
v, b': nat
b'': natlist
B: b = b' :: b''
IHb'': b = b'' ->
count v (add v b'') = count v b'' + 1
x:= if v =? b' then S (count v b'') else count v b'': nat
S x = x + 1

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.
b: bag
v, b': nat
b'': natlist
B: b = b' :: b''
IHb'': b = b'' ->
count v (add v b'') = count v b'' + 1
x:= if v =? b' then S (count v b'') else count v b'': nat
S x = x + 1

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.

Answer (Ana Borges)

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.
Interpreting this declaration as if a global
declaration prefixed by "Local", i.e. as a global
declaration which shall not be available without
qualification when imported. [local-declaration,scope]
Variable count : nat -> nat -> nat.
Interpreting this declaration as if a global
declaration prefixed by "Local", i.e. as a global
declaration which shall not be available without
qualification when imported. [local-declaration,scope]

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.
S (if v =? b' then S (count v b'') else count v b'') =
(if v =? b' then S (count v b'') else count v b'') + 1
Proof.
S (if v =? b' then S (count v b'') else count v b'') =
(if v =? b' then S (count v b'') else count v b'') + 1
  set t := (X in S X = X + _).
t:= if v =? b' then S (count v b'') else count v b'': nat
S t = t + 1
  Undo.
S (if v =? b' then S (count v b'') else count v b'') =
(if v =? b' then S (count v b'') else count v b'') + 1
  set t := match _ with true => _ | false => _ end.
t:= if v =? b' then S (count v b'') else count v b'': nat
S t = t + 1

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

  set (t := match _ with true => _ | false => _ end).
t:= if v =? b' then S (count v b'') else count v b'': nat
S t = t + 1