# Proving obvious logic

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.

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

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)

Thanks
Lil

Any help please ? or some guidelines ?

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

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