Proving obvious logic

Using Coq
1

Hello all,

I am working on the following code (I’m still new to Coq and proofs)

(START)
Require Import Lists.List.
Import ListNotations.
Require Import Coq.Arith.Arith.
Require Import Lia.

Record X := { a : nat; b : nat }.

Definition Xlist := list X.

Definition Xrecord1 := Build_X 1 2.
Definition Xrecord2 := Build_X 3 5.
Definition Erecord := Build_X 0 0.

Definition xl : Xlist := [Xrecord1; Xrecord2].
Compute xl.

Definition eq_X (x1 x2 : X) : bool :=
(Nat.eqb x1.(a) x2.(a)) && (Nat.eqb x1.(b) x2.(b)).

(* Find the position of an element in a list using equality *)
Fixpoint position_of_X (x : X) (l : list X) : nat :=
match l with
| => 0
| y :: ys => if eq_X x y then 1
else match position_of_X x ys with
| 0 => 0
| pos => S pos
end
end.

Compute position_of_X Xrecord1 xl.
Compute position_of_X Xrecord2 xl.
Compute nth 1 xl Erecord.

Inductive answer : Type := | yes : answer | no : answer | neutral : answer.

Definition Answer (x1 x2 : X) : answer :=
match Nat.compare x1.(a) x2.(a) with
| Eq => match Nat.compare x1.(b) x2.(b) with
| Eq => neutral
| Gt => yes
| Lt => no
end
| Gt => yes
| Lt => no
end.

Fixpoint ListAnswer (l1 l2 : nat)(xl1 xl2 : Xlist): answer := (* l1, l2 : lengths of xl1, xl2 *)
if l1 <=? l2 then
match l1, l2 with
| O, O | _, O => neutral
| O, _ => no
| S l1’, S l2’ => match Answer (nth l1’ xl1 Erecord) (nth l1’ xl2 Erecord) with
| neutral => ListAnswer l1’ l2’ xl1 xl2
| yes => yes
| no => no
end
end
else
match l1, l2 with
| O, O | O, _ => neutral
| _, 0 => yes
| S l1’, S l2’ => match Answer (nth l2’ xl1 Erecord) (nth l2’ xl2 Erecord) with
| neutral => ListAnswer l1’ l2’ xl1 xl2
| yes => yes
| no => no
end
end.

Definition Property (l1 l2 : nat) (xl1 xl2 : Xlist) :=
l1 < l2 /\ ListAnswer l1 l2 xl1 xl2 = no → (forall n, n < l1 → Answer (nth n xl1 Erecord) (nth n xl2 Erecord) <> yes).

Lemma test : forall (l1 l2 : nat) (xl1 xl2 : Xlist),
l1 < l2 /\ Property l1 l2 xl1 xl2 /\ ListAnswer l1 l2 xl1 xl2 = no →
ListAnswer l1 (S l2) xl1 xl2 = no.

(** END**)

Basically, in the ListAnswer function, I compare the 2 lists lengths and do some comparison based on the smallest one.
In the Lemma test, what I am saying is that, if l1 < l2 then the comparison will always be fixed by l1, so with l1 and (S l2), the outcome will remain the same.
However when working on the proof I get stuck at 1 particular case :frowning:

PS : I also cannot make good use of the Property, I tried specialize tactic but it’s not doing the job.

PS2: Can you tell me how to write the property in a different (more useful way) if it helps in the proof (though I would still be stuck elsewhere)

Any help please ?
Thanks
Lil

2

Any help please ? or some guidelines ?

3

A few points:

  1. You probably want to use List.length to get the length of your list.
  2. In the final lemma, it is not sure what l2 represents, since if it is the length of xl2, then doing S l2 on xl2 should have undefined behavior.

As an example fix, your “Property” should look something like

Lemma Property (xl1 xl2 : Xlist) :=
List.length xl2 < List.length xl2 ->
ListAnswer xl1 xl2 = no ->
(forall n, n < (List.length xl1) -> ...).
Proof. ...
  1. Following a similar vein, “length annotations” can be removed from everywhere, and in particular in ListAnswer, you could do a match on the lists themselves, which is much more direct:
match xl1, xl2 with
| [], [] => ...
| [], _ => ...
| _, [] => ...
| x1h::x1t, x2h::x2t => (* recursive on x1t, x2t *)

Once your code is more “functional”, you might find proofs simpler to do.

1 Like
4

I agree @yjtan. Thank you for this amazing solution.