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

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