De acordo com o manual coq, a tática de desdobramento realiza a redução delta em uma definição, seguida por várias outras reduções, incluindo a redução beta.
Parece que às vezes, para desencadear a redução beta após a redução delta no desdobramento, você precisa primeiro destruir um argumento.
Por exemplo, no lema ' desdobrar_lemma ' abaixo, o primeiro ' desdobrar myFunction ' (comentado no código) não parece acionar a redução beta, enquanto a redução beta é realizada após a destruição do argumento t.
Obviamente há algo que não entendo com a redução beta. Alguém pode me ajudar a esclarecer esse ponto?
Inductive tree : Type :=
| tree_cons : list tree -> tree.
Fixpoint andAll (ls: list bool) : bool :=
match ls with
| nil => true
| cons h t => andb h (andAll t)
end.
Definition isLeaf (t: tree) : bool :=
match t with
| tree_cons l => match l with
| nil => true
| x::rest => false
end
end.
Definition isSpecial (t: tree) : bool :=
match t with
| tree_cons l => match l with
| nil => false
| x::rest => andAll (map isLeaf l)
end
end.
Section flat_map_index.
Variables A B : Type.
Variable f : nat -> A -> list B.
Fixpoint flat_map_index (n:nat) (l:list A) : list B :=
match l with
| nil => nil
| cons x t => (f n x)++(flat_map_index (S n) t)
end.
End flat_map_index.
Fixpoint myFunction (l:list nat) (index:nat) (t: tree) : list (list nat) :=
let l' := (l++[index]) in
if (isSpecial t) then
match l' with
| [] => []
| xx::rest => [rest]
end
else
match t with
| tree_cons subtrees => flat_map_index (myFunction l') O subtrees
end.
Lemma unfold_lemma: forall a,
In [0] (myFunction [0] 0 a) -> isSpecial a = true.
Proof.
intro t.
(* unfold myFunction. *)
destruct t as [subtrees].
unfold myFunction.
fold myFunction.
destruct (isSpecial (tree_cons subtrees)) eqn:HCase.
+ easy.
+ ...
A redução beta substitui argumentos em abstrações lambda. As abstrações Lambda não podem ser recursivas.
myFunction, sendo umFixpoint, o delta se reduz a umafixexpressão, que é distinta de uma abstração lambda (fun).fixas expressões são avaliadas usando o que Coq chama de redução iota , não redução beta. A redução de Iota reduz a aplicação de um ponto fixo apenas quando o argumento decrescente do ponto fixo é liderado por um construtor.A distinção entre redução iota e beta garante uma forte normalização: se os pontos fixos fossem avaliados por meio da redução beta comum, de modo que pudessem se expandir quando o argumento decrescente não fosse um construtor, então você poderia expandir o ponto fixo dentro de si para sempre. O sistema ainda teria uma normalização fraca : para qualquer termo haveria sempre uma sequência de redução que termina com um valor. A forte propriedade de normalização, de que toda sequência de redução termina com um valor, pega fogo.
Algum código demonstrando o acima.
No seu código, o argumento decrescente
myFunctioné o terceiro,t : tree. Portanto,myFunction l index tsó reduzirá (ou seja, só sofrerá uma redução iota depois de ser reduzido em delta) quandotfor liderado portree_cons.Observe que você sempre pode provar explicitamente que uma
fixexpressão é igual à sua expansão. Você simplesmente não consegue fazer com que o Coq use automaticamente essa igualdade durante a conversão.Se você acha que seria útil, você pode escrever esse lema
myFunctione usá-lo em vez de confiar na conversão. Também ouvi dizer que o plugin Equations para Coq permite gerar tais lemas automaticamente, embora eu nunca o tenha usado.(De acordo com a documentação,
unfoldaplica-se a redução delta especificada e, em seguida, todas asletreduções beta, iota e zeta (simplifica s).)