The Coq mailing list

[Maxime Buyse <maxime.buyse AT prover.com>]

Hello !

I am working on a memory model with a state monad. But I fail to prove that the result of successive assignations in arrays is what I expect. After using the compute​ tactic, I do get the expected result and I can use reflexivity​ to prove the goal. But then Qed​ fails. Here is an example that I tried to minimize:

```

Require Import PArray.

Require Import Uint63.

Open Scope uint63_scope.

Definition mem := array (array int).

Definition SCM  := (mem -> mem) -> mem.

Definition run  : SCM -> mem                 := fun s     => s (fun x => x).

Definition ret  : mem -> SCM                 := fun x k   => k x.

Definition bind : SCM -> (mem -> SCM) -> SCM := fun s f k => s (fun m => f m k).

Definition m := (make 2 (A:=array int) (make 0 (A:=int) 0))

    .[0 <- (make 2 (A:=int) 0).[0<-20].[1<-21] ]

    .[1 <- (make 2 (A:=int) 0).[0<-30].[1<-31] ].

Definition m_expected := (make 2 (A:=array int) (make 0 (A:=int) 0))

    .[0 <- (make 2 (A:=int) 0).[0<-200].[1<-21] ]

    .[1 <- (make 2 (A:=int) 0).[0<-30].[1<-300] ].

Definition assign_instr :=

    bind

        (bind (ret m) (fun m => ret (m.[0 <- m.[0].[0 <- 200]])))

        (fun m_inter => bind (ret m_inter) (fun m => ret (m.[1 <- m.[1].[1 <- 300]]))).

Lemma test2 : run assign_instr = m_expected.
Proof. compute. reflexivity. Qed.

```

The error is:

```
The term "eq_refl" has type

 "[| [| 200; 21 | 0 : int |]; [| 30; 300 | 0 : int |] |

  [| | 0 : int |] : array int |] =

  [| [| 200; 21 | 0 : int |]; [| 30; 300 | 0 : int |] |

  [| | 0 : int |] : array int |]" while it is expected to have type

 "run assign_instr = m_expected".

```

From the documentation of Qed (https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Qed) I understand that this is quite unusual. If I change the order of my assignations in assign_instr​ the proof succeeds.

Where can this come from ?

I am using Coq 8.14.0

Thanks in advance !

Maxime