Двоичный поиск Дерево в Coq.Проблема в использовании (e0: (val? = N) = true), чтобы доказать val = n

Question

Как я уже сказал, у меня есть гипотеза e0 : (val =? n) = true, и я должен доказать, что 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)

Answer 1

Вы хотите использовать лемму beq_nat_true.

---

Если я выполню

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

Я вижу

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)

Вы также можете сделать

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

, которая дает вам леммы, которые содержат подтерм, соответствующий шаблону ((_ =? _) = true), который является подмножеством

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

Из них он выглядит как

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

делает что хочешь.Вы должны быть в состоянии решить вашу цель с любым из

• 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.

Если вы хотите превратить это в тактику, вы можете написать что-то вроде

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.