Stream: math-comp users

Topic: Proof of codomf_set


view this post on Zulip Ricardo (Nov 24 2022 at 20:54):

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.

view this post on Zulip Ricardo (Nov 24 2022 at 23:47):

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?

view this post on Zulip Paolo Giarrusso (Nov 25 2022 at 00:05):

the computation will at least be stuck on V which is a variable

view this post on Zulip Paolo Giarrusso (Nov 25 2022 at 00:08):

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
*)

view this post on Zulip Paolo Giarrusso (Nov 25 2022 at 00:11):

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
*)

view this post on Zulip Paolo Giarrusso (Nov 25 2022 at 00:17):

does this help?

view this post on Zulip Ricardo (Nov 25 2022 at 03:28):

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

view this post on Zulip Ricardo (Nov 25 2022 at 03:29):

Do you agree that fsval (fincl ks_sub [` H]) \in ks should evaluate to true in that context?

view this post on Zulip Paolo Giarrusso (Nov 25 2022 at 04:13):

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...

view this post on Zulip Paolo Giarrusso (Nov 25 2022 at 04:13):

You can try for yourself via:

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

view this post on Zulip Paolo Giarrusso (Nov 25 2022 at 04:13):

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

view this post on Zulip Paolo Giarrusso (Nov 25 2022 at 04:18):

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.

view this post on Zulip Paolo Giarrusso (Nov 25 2022 at 04:21):

simpler example:

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

view this post on Zulip Paolo Giarrusso (Nov 25 2022 at 04:22):

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).

view this post on Zulip Ricardo (Nov 25 2022 at 14:20):

Thank you very much Paolo :orange_heart:

view this post on Zulip Ricardo (Nov 25 2022 at 14:20):

I like this method for trying for myself. I had read about cbv before but hadn't seen what it could be useful for.

view this post on Zulip Ricardo (Nov 25 2022 at 14:20):

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

view this post on Zulip Ricardo (Nov 25 2022 at 14:23):

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.

view this post on Zulip Paolo Giarrusso (Nov 25 2022 at 14:46):

yes, propositional equality will be enough for your actual proof, but reduction tactics like simpl, change etc can only use definitional equalities.

view this post on Zulip Ricardo (Nov 25 2022 at 15:20):

I see. That's right. Thanks Paolo.

view this post on Zulip Ricardo (Nov 25 2022 at 15:43):

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