CODEWITHSUNDEEP
coq
laiba naz
laiba naz

Reputation: 57

Check less or equal natural number in coq

I have function (beq_nat_refl) which determines the equality of two natural numbers and gives a boolean. But now I want to prove a lemma stating that a natural number x is less or equal to x. May I use the above function (beq_nat_refl)? 

Theorem beq_nat_refl : 
  forall n : nat,
    true = beq_nat n n.

Theorem leq_nat :
  forall x:nat,
    x <= x.

Upvotes: 2

Views: 1901

Answers (2)

emi
emi

Reputation: 5410

Here is a straightforward path to proving leq_nat from similar definitions:

Fixpoint leb (n m : nat) : bool :=
  match n, m with
  | 0  , _   => true
  | _  , 0   => false
  | S n, S m => leb n m
  end.

Lemma leb_nat_refl : forall (n : nat), leb n n = true.
Proof.
  induction n; simpl.
  + reflexivity.
  + assumption.
Qed.

Lemma leb_nat_reflect : forall (n : nat), leb n n = true <-> n <= n.
Proof.
  induction n; simpl; split; intros.
  + constructor.
  + reflexivity.
  + constructor.
  + apply IHn. constructor.
Qed.

Theorem leq_nat : forall (n : nat), n <= n.
Proof.
  intros.
  apply leb_nat_reflect.
  apply leb_nat_refl.
Qed.

Upvotes: 0

ejgallego
ejgallego

Reputation: 6852

That would work if you would define x <= y as x < y || x == y; however this is not the definition, so usually the proof of x <= x tends to be induction [on the computational case] or by applying the base constructor if using a witness.

Upvotes: 1

Related Questions