Coq не уменьшит выражение, включающее процедуру принятия решения - PullRequest
Новая
       22

Coq не уменьшит выражение, включающее процедуру принятия решения

1 голос
/ 23 апреля 2019

Я использую Coq версии 8.8.1, и я не могу понять, почему он не будет оценивать значение следующих вычислений. 

Require Import Coq.Lists.List.
Import Coq.Lists.List.ListNotations.
Require Import Coq.Classes.EquivDec.
Require Import Coq.Init.Nat.
Require Import Coq.Arith.EqNat.
Require Import Coq.Lists.ListSet.
Require Import Coq.Bool.Bool.

Inductive term : Set :=
  | var : nat -> term
  | fn : nat -> term -> term.

Scheme Equality for term.

Fixpoint uf_find (x : term) (ufs : set (set term)) : option (set term) :=
  match ufs with
  | [] => None
  | uh::ufs' => match (set_In_dec term_eq_dec x uh) with
                | left _ _ => Some uh 
                | right _ _ => uf_find x ufs'
                end
  end.
Compute uf_find (var 3) nil.
(* Why isn't this fully reduced? *)
Compute uf_find (var 3) (cons nil nil).

Аналогичная функция с term_eq_dec вместо этого работает просто отлично: 

Fixpoint has_succ (x : nat) (l : list term) : option term :=
  match l with
  | [] => None
  | h::l'=> match term_eq_dec (var (S x)) h with
            | left _ _ => Some h
            | right _ _ => has_succ x l'
            end
  end.
Compute has_succ 3 [(var 2); (var 1); (var 4)].
...