coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Casteran <pierre.casteran AT labri.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] make coinductive types and hypotheses work together
- Date: Sun, 07 Aug 2011 16:51:09 +0200
Just a comment:
As Cedric showed, the hypothesis foo is useless.
First, an informal argument :
If you look at my_Inf, it defines the "biggest" set X of possibly infinite lists such that if Lcons 0 x belongs to X then x belongs to X.
Since the type LList is such a set, and is clearly the biggest one,
the predicate my_Inf characterizes all the elements of LList.
If you put it in Coq, you obtain the following proof.
CoInductive LList : Set :=
LNil : LList
| LCons : nat -> LList -> LList.
CoInductive my_Inf : LList -> Prop :=
My_Inf_Lcons : forall l, my_Inf (LCons 0 l) -> my_Inf l.
Lemma L : forall l, my_Inf l.
cofix.
split;apply L.
Qed.
Pierre
Quoting AUGER Cedric
<Cedric.Auger AT lri.fr>:
Le Sun, 7 Aug 2011 14:40:55 +0800,
Hongjin Liang
<lianghongjin AT gmail.com>
a écrit :
Hi all,
I defined a coinductive property and tried to prove a lemma about it.
When I applied the hypothesis, the proof violates the guarded
condition. But if I wrote the same hypothesis as a case in the
coinductive definition, then I can complete the proof. I'm not
familiar with coq, but I'm really curious about the reasons behind
the results and hope somebody could help me. My code is given below
(it itself does not have special meanings).
*****************************************************************************
CoInductive LList : Set :=
LNil : LList
| LCons : nat -> LList -> LList.
CoInductive my_Inf : LList -> Prop :=
My_Inf_Lcons : forall l, my_Inf (LCons 0 l) -> my_Inf l.
Hypothesis foo : forall l, my_Inf l -> my_Inf (LCons 0 l).
Lemma foo_test : forall l, my_Inf l.
Proof.
cofix H. intros. apply My_Inf_Lcons. apply foo. apply H. Guarded.
------------------------------------------------------------------------------------------------
The error message:
Recursive definition of H is ill-formed.
In environment
H : forall l : LList, my_Inf l
l : LList
Sub-expression "foo l (H l)" not in guarded form (should be a
constructor, an
abstraction, a match, a cofix or a recursive call).
Recursive definition is: "fun l : LList => My_Inf_Lcons l (foo l (H
l))".
*****************************************************************************
Then I merged the coinductive definition my_Inf and the hypothesis
foo to be a new coinductive definition:
CoInductive my_Inf : LList -> Prop :=
My_Inf_Lcons : forall l, my_Inf (LCons 0 l) -> my_Inf l
| foo : forall l, my_Inf l -> my_Inf (LCons 0 l).
Lemma foo_test : forall l, my_Inf l.
Proof.
cofix H. intros. apply My_Inf_Lcons. apply foo. apply H. Guarded.
Qed.
The proof is completed and foo_test is defined.
*****************************************************************************
I'm really curious about the differences between the above two ways to
define and prove coinductive properties. Could anyone give me some
hints about the reasons behind the results please? Thanks a lot!
- Hongjin
I am not used to CoInductives, so it takes me some time to understand
the problem; consider this variation (just an instantiation of foo)
======================================================================
CoInductive LList : Set :=
LNil : LList
| LCons : nat -> LList -> LList.
CoInductive my_Inf : LList -> Prop :=
My_Inf_Lcons : forall l, my_Inf (LCons 0 l) -> my_Inf l.
Lemma foo : forall l, my_Inf l -> my_Inf (LCons 0 l).
now intros l [].
Defined.
(*Hypothesis foo : forall l, my_Inf l -> my_Inf (LCons 0 l).*)
Lemma foo_test : forall l, my_Inf l.
Proof.
intros l.
cofix H.
Guarded.
set (term := My_Inf_Lcons l (foo l H)).
unfold foo in term.
======================================================================
Now what would mean this proof?
That is I assume my final result by coinduction then destruct it then
rebuild it, so that there is a constructor at head of term.
But the truth is that really "built something" the coinduction doesn't
hold.
I did this artificial example, which roughly follows what you did:
CoInductive dummy : Set :=
Dummy: False -> dummy.
(*
CoFixpoint dummy_wrong: dummy.
cofix H.
(* apply H. Guarded. *)
apply Dummy.
Guarded.
destruct H.
Guarded.
*)
Hypothesis foo: dummy -> False.
(* you can instantiate it with destructing the argument. *)
(*Lemma foo: dummy -> False. now intros []. Qed.*)
Lemma foo_test : dummy.
cofix H.
apply Dummy.
apply foo.
apply H.
Guarded.
The guardness condition requires that the corecursive call is not
inspected; so it cannot be argument of an opaque function or a
transparent inspecting function.
In your second definition, there is no inspection, only a sequence of
constructor and it is ok.
To convince you, try to write manually the first constructors of your
first definition (you won't be able to do so).
Your second attempt gives a term of the form
My_Inf_Lcons l (foo (Lcons 0 l) (My_Inf_Lcons (Lcons 0 …)))
foo is no more an hypothesis, but a constructor
- [Coq-Club] make coinductive types and hypotheses work together, Hongjin Liang
- Re: [Coq-Club] make coinductive types and hypotheses work together,
AUGER Cedric
- Re: [Coq-Club] make coinductive types and hypotheses work together, Pierre Casteran
- Re: [Coq-Club] make coinductive types and hypotheses work together,
AUGER Cedric
Archive powered by MhonArc 2.6.16.