Hi. I'm trying to prove some basic facts about finite maps from mathcomp.finmap. The lemma I want to prove is similar to `codomf_set`

, so I just copy-pasted it into my code to see how's working. However, when I did that the proof doesn't go through.

```
From mathcomp Require Import ssreflect ssrbool ssrnat ssrfun eqtype choice fintype seq finfun finmap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module ContactGraphs.
Local Open Scope fset.
Local Open Scope fmap.
(* finite maps *)
Section FinMap.
Variables (K V : choiceType).
(* add many keys pointing to the same value *)
(* Fixpoint setks (m : {fmap K -> V}) (ks : seq K) (v : V) := *)
(* if ks is k :: ks' then setks m.[k <- v] ks' v else m. *)
(* very similar to setf in mathcomp.finmap *)
Definition setks (m : {fmap K -> V}) (ks : {fset K}) (v : V) :=
[fmap k : ks `|` domf m =>
if val k \in ks then v
else odflt v (fnd m (val k))].
Definition getks (m : {fmap K -> V}) (v : V) : {fset K} :=
[fset k | k in m & m.[? k] == Some v].
Lemma setksD (m : {fmap K -> V}) (ks : {fset K}) (v : V) :
domf (setks m ks v) = ks `|` domf m.
Proof using Type. done. Qed.
Lemma setksC (m : {fmap K -> V}) (ks : {fset K}) (v : V) :
codomf (setks m ks v) = v |` codomf m.[\ ks].
Proof using Type.
apply/fsetP=> v'. rewrite !inE.
have [-> | neq_v'v] /= := altP eqP.
Admitted.
Lemma codomf_set f (k : K) (v : V) (kf : k \in domf f) :
codomf f.[k <- v] = v |` codomf f.[~ k].
Proof.
rewrite -setf_rem1. apply/fsetP=> v'. rewrite !inE.
have [->|neq_v'v] /= := altP eqP.
(* by apply/codomfP; exists k; rewrite fnd_set eqxx. *) (* error: cannot apply view codomfP *)
(* so I tried to continue the proof on my own, but ... *)
apply/existsP. exists k. (* Coq can't tell that k belongs to the finite set k |` ... *)
```

The error I get in the last line is

```
The term "k" has type
"let (sort, _) := K in sort"
while it is expected to have type
"Finite.sort
(k
|` [fset x
| x in domf f
& x \in domf f `\ k])".
```

Any help understanding what's going on here would be much appreciated. Either why the code as published in github isn't working in my setup or how we could proceed with the new proof.

I got a bit further trying to prove lemma `setksC`

. I get to a point where I'd think Coq can just evaluate and finish the current sub-goal, but it can't apparently.

```
Lemma setksC (m : {fmap K -> V}) (ks : {fset K}) (v : V) :
ks != fset0 ->
codomf (setks m ks v) = v |` codomf m.[\ ks].
Proof using Type.
move=> /fset0Pn [k H]. apply/fsetP=> v'. rewrite !inE.
have [eq_v'v | neq_v'v] /= := altP eqP.
apply/existsP.
have ks_sub : ks `<=` (ks `|` domf m) by rewrite fsubsetUl.
exists (fincl ks_sub [` H]).
Admitted.
```

The state at the end is

```
...
H : k \in ks
eq_v'v : v' = v
ks_sub : ks `<=` ks `|` domf m
============================
[ffun k0 => if fsval k0 \in ks
then v
else odflt v m.[? fsval k0]]
(fincl ks_sub [` H]) == v'
```

By beta-reduction, one should get `fsval (fincl ks_sub [` H]) \in ks`

which I'd think should evaluate to `true`

. Why isn't Coq able to perform these two reduction steps? What am I not seeing?

the computation will at least be stuck on `V`

which is a variable

a simpler example is that `fun v : V => v == v.`

should obviously be equal to `fun v : V => true`

, but it's not definitionally equal:

```
Eval cbv in fun v : V => v == v.
(*
= fun v : let (sort, _) := V in sort =>
(let (op, _) :=
Choice.base
(let
'@Choice.Pack sort c as cT' := V
return (Choice.class_of (let (sort, _) := cT' in sort)) in c) in
op) v v
: V -> bool
*)
```

feel free to ask further if that's unfamiliar.

Back to your goal, there `Set Printing All.`

shows

```
is_true
(@eq_op (Choice.eqType V) ...
```

and `eq_op`

needs to project the actual equality from `V`

:

```
Print eq_op.
(*
eq_op =
fun T : eqType => Equality.op (Equality.class T)
: forall T : eqType, rel T
*)
Eval cbv in @eq_op.
(*
Arguments eq_op {T} _ _
= fun T : eqType =>
let (op, _) :=
let
'EqType sort c as cT := T
return (Equality.mixin_of (let (sort, _) := cT in sort)) in c in
op
: forall T : eqType, rel T
*)
```

does this help?

If I understand correctly what you're saying, you're talking about the part of the goal that says `... == v'`

. Is that correct?

Do you agree that `fsval (fincl ks_sub [` H]) \in ks`

should evaluate to `true`

in that context?

Maybe you can _prove_ that's they're propositionally equal, but they're definitely not definitionally equal: to run that computation Coq would need to know `ks`

, `k`

and `K`

's comparison...

You can try for yourself via:

```
set x := fsval (fincl ks_sub [` H]) \in ks.
cbv in x.
```

what I get is:

```
x:= (fix mem_seq (s : seq (let (sort, _) := K in sort)) :
(let (sort, _) := K in sort) -> bool :=
match s with
| [::] => xpred0
| y :: s' =>
fun x : let (sort, _) := K in sort =>
if
(let (op, _) :=
Choice.base
(let
'@Choice.Pack sort c as cT' := K
return (Choice.class_of (let (sort, _) := cT' in sort))
in c) in
op) x y
then true
else mem_seq s' x
end) (let (enum_fset, _) := ks in enum_fset) k : bool
```

What does work is this:

```
set x := fsval (fincl ks_sub [` H]) \in ks.
change (fsval (fincl ks_sub [` H]) \in ks) with (mem_seq ks k) in x.
```

that gives `x:= mem_seq ks k : bool`

, and I can see how `H: k \in ks`

_implies_ `x`

will be _propositionally_ equal to `true`

. But that's not a definitional equality: since `mem_seq`

only reduces by (delta)-zeta reduction (fixpoint reduction), the proof must be by induction on `ks`

.

simpler example:

```
Lemma foo (n : nat) : n == n.
Proof. Fail reflexivity.
cbv.
Fail reflexivity.
Undo.
Undo.
done.
```

here, it's maybe misleading that `done`

succeeds, but that's just because there's a _lemma_ that applies, as shown by continuing with:

```
Undo.
info_trivial.
(* info trivial: *)
simple apply eqxx (in core).
```

Thank you very much Paolo :orange_heart:

I like this method for trying for myself. I had read about `cbv`

before but hadn't seen what it could be useful for.

I think propositional equality would be enough for what I'm trying to achieve right?

However, there are a few gaps I need to fill yet. The first thing I don't know how to do is how to beta-reduce the expression involving a finite function in the goal, so that I get the `fsval (fincl ks_sub [` H]) \in ks`

inside the `if`

, that I can then replace with `change`

. I'll ask that in a separate question.

yes, propositional equality will be enough for your actual proof, but reduction tactics like `simpl`

, `change`

etc can only use definitional equalities.

I see. That's right. Thanks Paolo.

I think my intuition was somewhat correct. By doing `rewrite ffunE /=`

the goal became `(if k \in ks then v else odflt v m.[? k]) == v'`

.

Last updated: Jan 29 2023 at 18:03 UTC