Lección de Funciones y recursividad.

Funciones

C:\freire\c98-99\md2>coqtop
Welcome to Coq V6.2.2 (September 1998)

Coq < Definition predecesor1: nat->nat :=
Coq <     [n:nat]Cases n of
Coq <           O =>O
Coq <       |(S p)=>p
Coq <            end.
predecesor1 is defined

Coq < Recursive Definition predecesor2: nat -> nat :=
Coq < O => O
Coq < |(S p)=> p.
predecesor2_eq1 is defined
predecesor2_eq2 is defined
predecesor2 is recursively defined.

Coq < Fixpoint predecesor3 [n:nat]:nat :=
Coq < Cases n of
Coq < O=>O
Coq < |(S p)=> p
Coq < end.
Warning: predecesor3 is non-recursively defined

Coq < Eval Compute in (predecesor1 (S (S O))).
= (S O)
: nat

Coq < Eval Compute in (predecesor2 (S (S O))).
= (S O)
: nat

Coq < Eval Compute in (predecesor3 (S (S O))).
= (S O)
: nat

Coq < Fixpoint f [C:Set;f0:C;fc:C->C;n:nat]: C :=
       Cases n of
            O => f0
        |(S p)=> (fc (f C f0 fc p))
       end.
f is recursively defined

Coq < Recursive Definition plus:nat->nat->nat:=
Coq < O b => b
Coq < |(S a) b => (S (plus a b)).
plus_eq1 is defined
plus_eq2 is defined
plus is recursively defined.

Coq < Definition f:= [x:nat](plus (2) x).
f is defined

Coq < Check f.
f
: nat->nat

Coq < Eval Compute in (f (89)).
= (91)
: nat

Coq < Recursive Definition plus : nat->nat->nat :=
Coq < O b => b
Coq < |(S a) b => (S (plus a b)).
plus_eq1 is defined
plus_eq2 is defined
plus is recursively defined.

Coq < Eval Compute in (plus (S O) (S O)).
= (S (S O))
: nat

La táctica Simpl trata de reducir el objetivo utilizando el valor de funciones.

Referencias

SIMPL This tactic applies to any goal. The tactic Simpl first applies beta i -reduction rule. Then it expands transparent constants and tries to reduce T' according, once more, to beta i rules. But when the i rule is not applicable then possible delta-reductions are not applied. For instance trying to use Simpl on (plus n O)=n will change nothing.