Stream: Coq users

Topic: Simplifying SSReflect Matrix


view this post on Zulip Mukesh Tiwari (May 07 2022 at 12:30):

Hi everyone, I have this goal and when I am using simpl, it not simplifying. How can I simplify this expression to apply induction hypothesis?

cons (Vector.t R n) vhd m vtl =
finite_fun_to_matrix
   (i : t n) (j : t m.+1),
     (\matrix_(i0, j0) matrix_to_finite_fun (cons (Vector.t R n) vhd m vtl)
                         (ord_to_finite i0) (ord_to_finite j0))%R
       (finite_to_ord i) (finite_to_ord j))


Lemma matrix_back_and_forth_same :
    forall (n m : nat) (mx : Matrix n m),
    mx = matrix_to_Matrix (Matrix_to_matrix mx).
  Proof.
    intros ? ?.
    revert n.
    induction m.
    + intros ? ?.
      unfold Matrix in mx.
      pose proof (vector_inv_0 mx) as Hn.
      subst; reflexivity.
    + intros ? ?.
      unfold Matrix in mx.
      destruct (vector_inv_S mx) as (vhd & vtl & vp).
      subst.
      unfold matrix_to_Matrix,
      Matrix_to_matrix.
      (* how to simplify *)

Complete Source Code:

Require Import Field_theory
  Ring_theory List NArith
  Ring Field Utf8 Lia
  Coq.Arith.PeanoNat
  Vector Fin.
From mathcomp Require Import
  all_ssreflect algebra.matrix
  algebra.ssralg.

Import ListNotations.

Set Implicit Arguments.


Section Mat.


  Variable (R : Type).

  Lemma vector_inv_0 (v : Vector.t R 0) :
    v = @Vector.nil R.
  Proof.
    refine (match v with
            | @Vector.nil _ => _
            end).
    reflexivity.
  Defined.

  Lemma vector_inv_S (n : nat) (v : Vector.t R (S n)) :
    {x & {v' | v = @Vector.cons _ x _ v'}}.
  Proof.
    refine (match v with
            | @Vector.cons _ x _ v' =>  _
            end).
    eauto.
  Defined.

  Lemma fin_inv_0 (i : Fin.t 0) : False.
  Proof. refine (match i with end). Defined.

  Lemma fin_inv_S (n : nat) (i : Fin.t (S n)) :
    (i = Fin.F1) + {i' | i = Fin.FS i'}.
  Proof.
    refine (match i with
            | Fin.F1 _ => _
            | Fin.FS _ _ => _
            end); eauto.
  Defined.


  Definition vector_to_finite_fun :
    forall n, Vector.t R n -> (Fin.t n -> R).
  Proof.
    induction n.
    + intros v f.
      apply fin_inv_0 in f.
      refine (match f with end).
    + intros v f.
      destruct (vector_inv_S v) as (vhd & vtl & vp).
      destruct (fin_inv_S f) as [h | [t p]].
      exact vhd.
      exact (IHn vtl t).
  Defined.


  Definition finite_fun_to_vector :
    forall n,  (Fin.t n -> R) -> Vector.t R n.
  Proof.
    induction n.
    + intros f.
      apply Vector.nil.
    + intros f.
      apply Vector.cons.
      apply f, Fin.F1.
      apply IHn;
      intro m.
      apply f, Fin.FS, m.
  Defined.


  Lemma finite_fun_to_vector_correctness
    (m : nat) (f : Fin.t m -> R) (i : Fin.t m) :
    Vector.nth (finite_fun_to_vector f) i = f i.
  Proof.
    induction m.
    - inversion i.
    - pose proof fin_inv_S i as [-> | (i' & ->)].
      + reflexivity.
      + cbn.
        now rewrite IHm.
  Defined.


  Lemma vector_to_finite_fun_correctness
    (m : nat) (v : Vector.t R m) (i : Fin.t m) :
    Vector.nth v i = (vector_to_finite_fun v) i.
  Proof.
    induction m.
    - inversion i.
    - pose proof fin_inv_S i as [-> | (i' & ->)].
      destruct (vector_inv_S v) as (vhd & vtl & vp).
      rewrite vp.
      reflexivity.
      destruct (vector_inv_S v) as (vhd & vtl & vp).
      rewrite vp;
      simpl;
      now rewrite IHm.
  Defined.

  Lemma vector_finite_back_forth :
    forall (n : nat) (v : Vector.t R n),
    v = finite_fun_to_vector (vector_to_finite_fun v).
  Proof.
    induction n.
    + intros v.
      pose proof (vector_inv_0 v) as Hv.
      subst;
      reflexivity.
    + intros v.
      destruct (vector_inv_S v) as (vhd & vtl & vp).
      subst; simpl; f_equal.
      apply IHn.
  Defined.




End Mat.


Section Mx.

  Variable (R : Type).

  Definition Matrix n m := Vector.t (Vector.t R n) m.

  Definition finite_fun_to_matrix {n m}
    (f : Fin.t n -> Fin.t m -> R) : Matrix n m :=
    @finite_fun_to_vector _ m (fun (x : Fin.t m) =>
      @finite_fun_to_vector _ n (fun (y : Fin.t n) => f y x)).

  Definition matrix_to_finite_fun {n m}
    (mx : Matrix n m) : Fin.t n -> Fin.t m -> R :=
    fun (x : Fin.t n) (y : Fin.t m) =>
      @vector_to_finite_fun _ n
        ((@vector_to_finite_fun _ m mx) y) x.

  Lemma matrix_to_finite_back_forth :
    forall n m (mx : Matrix n m),
    mx = finite_fun_to_matrix (matrix_to_finite_fun mx).
  Proof.
    intros ? ?.
    revert n.
    induction m.
    + intros ? ?.
      unfold Matrix in mx.
      pose proof (vector_inv_0 mx) as Hn.
      subst; reflexivity.
    + intros ? ?.
      unfold Matrix in mx.
      destruct (vector_inv_S mx) as (vhd & vtl & vp).
      subst.
      unfold finite_fun_to_matrix,
      matrix_to_finite_fun.
      simpl; f_equal.
      apply vector_finite_back_forth.
      apply IHm.
  Defined.


  Definition finite_to_ord {n} (f : Fin.t n) : 'I_n.
    have [m Hm] := (to_nat f).
    apply (introT ltP) in Hm.
    apply (Ordinal Hm).
  Defined.

  Definition ord_to_finite {n} (x : 'I_n) : Fin.t n.
    have Hx: x < n by [].
    apply (elimT ltP) in Hx.
    apply (of_nat_lt Hx).
  Defined.

  Definition Matrix_to_matrix {n m}
    (mx : Matrix n m) : 'M[R]_(n, m) :=
    \matrix_(i < n, j < m)
      (matrix_to_finite_fun
        mx
        (ord_to_finite i)
        (ord_to_finite j)).

  Definition matrix_to_Matrix {n m}
    (mx : 'M[R]_(n, m)) : Matrix n m :=
    finite_fun_to_matrix (fun (i : Fin.t n)
      (j : Fin.t m) =>
      mx (finite_to_ord i) (finite_to_ord j)).


  Lemma matrix_to_Matrix_correctness :
    forall n m (i : Fin.t n) (j : Fin.t m)
    (mx : 'M[R]_(n, m)),
    mx (finite_to_ord i) (finite_to_ord j) =
    Vector.nth (Vector.nth (matrix_to_Matrix mx) j) i.
  Proof.
    intros *.
    unfold matrix_to_Matrix,
    finite_fun_to_matrix.
    rewrite finite_fun_to_vector_correctness.
    rewrite finite_fun_to_vector_correctness.
    reflexivity.
  Defined.

  Lemma matrix_back_and_forth_same :
    forall (n m : nat) (mx : Matrix n m),
    mx = matrix_to_Matrix (Matrix_to_matrix mx).
  Proof.
    intros ? ?.
    revert n.
    induction m.
    + intros ? ?.
      unfold Matrix in mx.
      pose proof (vector_inv_0 mx) as Hn.
      subst; reflexivity.
    + intros ? ?.
      unfold Matrix in mx.
      destruct (vector_inv_S mx) as (vhd & vtl & vp).
      subst.
      unfold matrix_to_Matrix,
      Matrix_to_matrix.
    (* This simp
      simpl.

view this post on Zulip Karl Palmskog (May 07 2022 at 15:35):

the standard answer is to try other evaluation approaches, like cbn, compute/cbv, etc.

view this post on Zulip Mukesh Tiwari (May 07 2022 at 17:50):

Thanks @Karl Palmskog . cbn worked but it's not simplifying the terms to the point that I can apply reflexivity or induction hypothesis. compute ran for 8 minutes and did nothing before I killed it. For example, the right hand side of the below expression should reduct to vhd but apparently, it's not happening.

vhd =
finite_fun_to_vector
   y : t n,
     (\matrix_(i, j) matrix_to_finite_fun (cons (Vector.t R n) vhd m vtl)
                       (ord_to_finite i) (ord_to_finite j))%R
       (finite_to_ord y) (Ordinal (n:=m.+1) (m:=0) (erefl true)))

view this post on Zulip Karl Palmskog (May 07 2022 at 18:11):

if it's slow, you can try vm_compute, or even native_compute if you have coq-native in opam (recommend different opam switch)

view this post on Zulip Karl Palmskog (May 07 2022 at 18:13):

some definitions will not reduce because they are "locked" (by library maintainers), not sure if this is happening here

view this post on Zulip Mukesh Tiwari (May 07 2022 at 18:23):

I figured out that introT, and similarly elimT, are opaque so I wrote one that reduces, using Defined (I also feel something like this happening, and hopefully I will figure it out).

An orthogonal question: is there any rationale behind using Qed in proofs?

view this post on Zulip Karl Palmskog (May 07 2022 at 18:34):

Qed is used for several reasons, not least:

view this post on Zulip Mukesh Tiwari (May 07 2022 at 18:38):

Do you think it's a good idea to have same theorem with two versions: one with Qed and one with Defined?

view this post on Zulip Karl Palmskog (May 07 2022 at 18:39):

if you know you need to access (compute with) the body of the constant somewhere else, go with Defined. Otherwise, I'd go with Qed until you find out you need something different

view this post on Zulip Karl Palmskog (May 07 2022 at 18:42):

even though it's a classic problem in Coq that some constants won't unfold, I think the problem of over-unfolding can be a serious issue (proof context becomes a mess). Qed can be a way to manage over-unfolding (but for more advanced unfold mitigation, locking is probably the way to go)

view this post on Zulip Mukesh Tiwari (May 08 2022 at 13:37):

Is this what you meant by locked @Karl Palmskog ?

mx =
  finite_fun_to_vector
     x : t m,
       finite_fun_to_vector
          y : t n,
            locked_with matrix_key (* SEE HERE *)
              (matrix_of_fun_def (m:=n) (n:=m))
               (i : ordinal_finType n)
                 (j : ordinal_finType m),
                 vector_to_finite_fun
                   (vector_to_finite_fun mx
                      (ord_to_finite j))
                   (ord_to_finite i))
              (finite_to_ord y) (finite_to_ord x)))

view this post on Zulip Karl Palmskog (May 08 2022 at 13:54):

right, yes, that looks like a library locking. This was a library designer choice so that one can't unfold, only use lemmas

view this post on Zulip Karl Palmskog (May 08 2022 at 13:54):

you could search for "locked definition" or similar in this stream or the MathComp stream, I know people talk about it form time to time. I don't know the technicalities

view this post on Zulip Li-yao (May 08 2022 at 14:28):

https://github.com/math-comp/hierarchy-builder/wiki/Locking says you can try rewrite unlock

view this post on Zulip Mukesh Tiwari (May 08 2022 at 16:18):

Thanks @Li-yao and @Karl Palmskog .

rewrite unlock did not work, and these are the relevant definitions in matrix. However, I could not find any lemma but I am not expert in math-comp so I might be missing something obvious.

Definition matrix_of_fun k := locked_with k matrix_of_fun_def.
Canonical matrix_unlockable k := [unlockable fun matrix_of_fun k].

view this post on Zulip Mukesh Tiwari (May 08 2022 at 16:37):

Nevermind, I just unfolded the locked definition and get rid of it by destructing it.

 (n m : nat) (mx : Matrix n m),
  mx =
  finite_fun_to_vector
     x : t m,
       finite_fun_to_vector
          y : t n,
            (let 'tt := matrix_key in λ (T : Type) (x0 : T), x0)
              ((ordinal_finType n  ordinal_finType m  R)  'M_(n, m))
              (matrix_of_fun_def (m:=n) (n:=m))
               (i : ordinal_finType n) (j : ordinal_finType m),
                 vector_to_finite_fun
                   (vector_to_finite_fun mx (ord_to_finite j))
                   (ord_to_finite i)) (finite_to_ord y)
              (finite_to_ord x)))

Very interesting way to not let definition unfold.

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 08:25):

Karl Palmskog said:

Qed is used for several reasons, not least:

Is that actually true? I thought it was only that the ones from other files don't get loaded from disk

view this post on Zulip Karl Palmskog (May 09 2022 at 08:28):

I've heard it was true at some point in Coq history, but you may be right that nowadays it only affects other files

view this post on Zulip Karl Palmskog (May 09 2022 at 08:29):

hence you get these absurdly huge files which take 10GB memory to run coqc on, but then you don't care once they are compiled

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 09:21):

I don't think that Qed proofs were ever removed from the memory of a coqc process. But you're right that their loading is deferred when requiring a vo, which is an important feature.

view this post on Zulip Karl Palmskog (May 09 2022 at 09:23):

but you could theoretically make the proof term inaccessible (and thus marked for GC) as soon as Qed is reached, right?

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 09:23):

theoretically, yes

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 09:24):

unfortunately the STM is a mess beyond repair

view this post on Zulip Ali Caglayan (May 09 2022 at 10:59):

Its not entirely correct that Qed can be GCed safely tho right? For example, extraction is able to peek behind Qed's (which is another design issue in itself). https://github.com/coq/coq/issues/15874

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 11:01):

the idea is that it can be swapped to disk (but not by the OS which doesn't have the info)

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 11:01):

not gc'd completely away


Last updated: Jan 29 2023 at 06:02 UTC