CODEWITHSUNDEEP
coq
Celthim
Celthim

Reputation: 13

Binary search Tree in Coq. Trouble to use ( e0 : (val ?= n) = true ) to prove val = n

As I said I have on hypothesis e0 : (val =? n) = true and I have to prove val = n

Inductive is_found : nat -> abr -> bool -> Prop :=
|is_not_found_nil : forall (n : nat), (is_found n nil false)
|is_found_node_eq : forall (n val : nat) (fg fd : abr), val = n -> (is_found n (Node val fg fd) (val =? n))
|is_found_node_lt : forall (n val : nat) (fg fd : abr) (res : bool), val > n -> (is_found n fg res) -> (is_found n (Node val fg fd) res)
|is_found_node_gt : forall (n val : nat) (fg fd : abr) (res : bool), val < n -> (is_found n fd res) -> (is_found n (Node val fg fd) res).

(* fonction *)
Fixpoint find (n : nat) (a : abr) : bool :=
match a with
|nil => false
|(Node val f1 f2) => if (val =? n) then true else match (lt_dec val n) with
                                |left _ => (find n f2)
                                |right _ => (find n f1)
                                end
end.

Functional Scheme find_ind := Induction for find Sort Prop.

Goal forall (n : nat) (a : abr), (is_found n a (find n a)).
induction a.
simpl.
apply is_not_found_nil.
functional induction (find n (Node n0 a1 a2)) using find_ind.
apply is_not_found_nil.
rewrite <- e0.
apply is_found_node_eq.



3 subgoals
n, n0 : nat
a1, a2 : abr
IHa1 : is_found n a1 (find n a1)
IHa2 : is_found n a2 (find n a2)
val : nat
f1, f2 : abr
e0 : (val =? n) = true
______________________________________(1/3)
val = n
______________________________________(2/3)
is_found n (Node val f1 f2) (find n f2)
______________________________________(3/3)
is_found n (Node val f1 f2) (find n f1)

Upvotes: 0

Views: 190

Answers (1)

Jason Gross
Jason Gross

Reputation: 6128

You want to use the lemma beq_nat_true.

If I execute

Require Import Coq.Arith.Arith.
Search "=?".

I see

Nat.eqb_refl: forall x : nat, (x =? x) = true
beq_nat_refl: forall n : nat, true = (n =? n)
Nat.eqb_sym: forall x y : nat, (x =? y) = (y =? x)
Nat.eqb_spec: forall x y : nat, Bool.reflect (x = y) (x =? y)
beq_nat_eq: forall n m : nat, true = (n =? m) -> n = m
beq_nat_true: forall n m : nat, (n =? m) = true -> n = m
Nat.eqb_eq: forall n m : nat, (n =? m) = true <-> n = m
beq_nat_false: forall n m : nat, (n =? m) = false -> n <> m
Nat.eqb_neq: forall x y : nat, (x =? y) = false <-> x <> y
Nat.eqb_compat:
  Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq))
    Nat.eqb
Nat.eqb_compare:
  forall x y : nat, (x =? y) = match x ?= y with
                               | Eq => true
                               | _ => false
                               end
Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
Nat.pow2_bits_eqb: forall n m : nat, Nat.testbit (2 ^ n) m = (n =? m)
Nat.setbit_eqb:
  forall a n m : nat,
  Nat.testbit (Nat.setbit a n) m = ((n =? m) || Nat.testbit a m)%bool
Nat.clearbit_eqb:
  forall a n m : nat,
  Nat.testbit (Nat.clearbit a n) m = (Nat.testbit a m && negb (n =? m))%bool
Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)

You could also do

Search ((_ =? _) = true).

which gives you the lemmas which contain a subterm matching the pattern ((_ =? _) = true), which is the subset

Nat.eqb_refl: forall x : nat, (x =? x) = true
beq_nat_true: forall n m : nat, (n =? m) = true -> n = m
Nat.eqb_eq: forall n m : nat, (n =? m) = true <-> n = m

Of these, it looks like

beq_nat_true: forall n m : nat, (n =? m) = true -> n = m

does what you want. You should be able to solve your goal with any of

  • now apply beq_nat_true.
  • auto using beq_nat_true.
  • apply beq_nat_true, e0.
  • apply beq_nat_true in e0; exact e0.
  • apply beq_nat_true in e0; subst; reflexivity.
  • now apply beq_nat_true in e0.

If you want to turn this into a tactic, you can write something like

Ltac beq_nat_to_eq :=
  repeat match goal with
         | [ H : (_ =? _) = true |- _ ] => apply beq_nat_true in H
         | [ H : (_ =? _) = false |- _ ] => apply beq_nat_false in H
         end.

Upvotes: 1

Related Questions