CODEWITHSUNDEEP
coq
sana sobia
sana sobia

Reputation: 19

check equality of natural number list pair

I have two natural number list pairs and want to check their equality.

Fixpoint beq_natlist (l1 l2 : list*list) : bool :=
 match l1, l2 with
| (nil , nil) => true
| (h :: nil, nil)  => false
| ( nil , h :: nil) => false
| h1 :: t1, h2 :: t2 => if beq_nat h1 h2 then beq_natlist t1 t2 else false

end.

Upvotes: 0

Views: 94

Answers (1)

Bubbler
Bubbler

Reputation: 982

First, equality of list nats would look like the following. Note that the multi-match pattern a, b and the pair notation (a, b) are two totally different things; the former matches two terms, while the latter matches one term which is a pair.

Fixpoint beq_natlist (l1 l2 : list nat) : bool :=
  match l1, l2 with
  | nil, nil => true
  | h :: nil, nil => false
  | nil, h :: nil => false
  | h1 :: t1, h2 :: t2 => if beq_nat h1 h2 then beq_natlist t1 t2 else false
  end.

Then you can use beq_natlist to build the equality of list nat * list nat:

Fixpoint beq_natlist_pair (p1 p2 : list nat * list nat) : bool :=
  match p1, p2 with
  | (l1, l2), (l3, l4) => beq_natlist l1 l3 && beq_natlist l2 l4
  end.

Upvotes: 1

Related Questions