Julin S (Jun 16 2022 at 06:11): Julin S (Jun 16 2022 at 06:11):This might seem like an weird exercise.
I got a set of functions:
I need the defintions to be like
Definition f (a b c:nat) : nat :=
let r0 := (p0 a b c) in
(* Would've been easy if this was possible *)
match r0 with
| True => 0
| False =>
let r1 := (p1 a b c) in
match r1 with
| True => 1
| False =>
let r2 := (p2 a b c) in
match r2 with
| True => 2
| False => 3
end
end
end
But this can't be done since we can't pattern match on Prop.
Would've been quite convenient if the p functions returned Type, I guess.
But I can't change the signatures of the functions.
What I need to do is to choose the return value of f based on three propositions.
0123Is there a way to do this?
Is using sigT a possible way?
The type of the functions can't be changed.
Julin S (Jun 16 2022 at 06:18):p0, p1, p2 could've been like:
Definition p0 (a b c:nat):Prop := a < b < c.
Definition p1 (a b c:nat):Prop := a > b > c.
Definition p2 (a b c:nat):Prop := a < b > c.
I have the impression you're trying to build an oracle function to get around the incompleteness theorems -- so I don't think that will work.
Julin S (Jun 16 2022 at 06:20):Actually, I was trying to put up a minimal example of a set of formulas that I had. I guess maybe posting it as such would be clearer.
Julien Puydt (Jun 16 2022 at 06:23):Can't your p0, p1 and p2 have boolean values?
Julin S (Jun 16 2022 at 06:27):I don't think so. But I may be wrong. I'll post the whole thing.
Julin S (Jun 16 2022 at 06:30):Give me a few minutes.
Julin S (Jun 16 2022 at 06:42):This is what I had been trying to encode in coq:
f:(nat -> option nat) -> (nat -> option nat) -> (nat -> option nat)
f a b = c
(* a b:nat->option nat *)
∀x:nat,
((c x) <> None) <->
∃x':nat, x' < x ->
(a x') = (x - x') /\
p0 x' /\
p1 x' x
∀x:nat,
(c x) = None <->
x' < x ->
(a x') <> (x - x') \/
(p2 x') \/
(p3 x' x)
-----
p0 : nat -> Prop
p0 x =
(c x) <> None \/
(b x) <> None
p1 : nat -> nat -> Prop
p1 x1 x2 =
∀x:nat,
x1 < x < x2 ->
(b x) = None
p2 : nat -> Prop
p2 x =
(c x) = None /\
(b x) = None
p3 : nat -> nat -> Prop
p3 x1 x2 =
∀x:nat,
x1 < x < x2 ->
(b x) <> None
How can I go about it? Been trying for some time, but without success.
Julin S (Jun 16 2022 at 06:43):Throughout, a and b are arguments of f. Likewise c is the return value of f.
Julien Puydt (Jun 16 2022 at 06:46):Your previous question had f compute something with the results of p*, but here it's the reverse, isn't it?
Julien Puydt (Jun 16 2022 at 06:47):The situation here seems much better: I see many x' < x which mean a bounded check, hence something that is a boolean.
Julien Puydt (Jun 16 2022 at 06:50):The declaration b: nat -> nat and the usage (b x) <> None don't seem coherent.
Julin S (Jun 16 2022 at 06:55):Sorry, all the (nat -> nat) should've been (nat -> option nat). Correcting.
Julin S (Jun 16 2022 at 06:58):The p functions got to be returning Prop, right? Since there are <> None usages and we can't have an isNone or isSome function. Or can we?
Kenji Maillard (Jun 16 2022 at 07:01):you can have
Definition isNone {A} (x : option A) : bool := match x with None => true | _ => false end.
and if you want to use isNone x as a proposition transparently, you can make the function is_true : bool -> Prop := fun b => b = true a coercion (that's one of the default setting if you were to load ssreflect), that is
Definition is_true : bool -> Prop := fun b => b = true.
Coercion is_true : bool >-> Sortclass.
:face_palm: I don't know what I had been thinking when I said we can't have isNone...
Julin S (Jun 16 2022 at 08:52):Oh, I was thinking of getSome: option A -> A.
Julin S (Jun 16 2022 at 09:11):Julien Puydt said:
The situation here seems much better: I see many
x' < xwhich mean a bounded check, hence something that is a boolean.
But those x < x' would have to be part of Prop values though, right?
For instance, p1 is something like:
Definition p1 (b:nat->option nat) (n1 n2:nat) : Prop :=
forall n:nat,
(n1 < n < n2) -> (* andb (Nat.ltb n1 n) (Nat.ltb n n2) *)
(b n) = None. (* (isNone (b n)) *)
There are at least 2 variations that are possible around getSome. The first is to take a default value in A, possibly with automation provided by typeclasses/canonical instances. The second is to take as an additional argument a proof that the given option is a Some (so you would have getSome : forall {A} (x : option A), isSome x -> A).
Julin S (Jun 16 2022 at 09:31):How would the version with proof look like:
This was my (incorrect) attempt:
Definition getSome_prf {A:Type} (default:A)
(x:option A) : isSome x -> A :=
(* Could we also just say [(x = Some _) -> A] ? *)
fun prf:(isSome (Some x')) => x'.
something like
match x with
| Some x => fun _ => x
| None => fun prf => (* use that prf is false in this branch *)
end
Can a complete standalone getSome_prf function be made like this?
Gaëtan Gilbert (Jun 16 2022 at 09:48):what does that mean?
Julin S (Jun 16 2022 at 09:49):I mean, I tried:
Definition getSome_prf {A:Type} (x:option A) : isSome x -> A :=
match x with
| Some x => fun _ => x
| None => fun prf =>
end.
But that gave error at the => of None's case.
Gaëtan Gilbert (Jun 16 2022 at 09:49):I didn't fill it in because I didn't look at what definition you used for isSome
Julin S (Jun 16 2022 at 09:49):where isSome is
Definition isNone {A:Type} (x:option A) : Prop :=
match x with
| None => True
| Some _ => False
end.
Definition isSome {A:Type} (x:option A) : Prop := not (isNone x).
Should it return bool?
Gaëtan Gilbert (Jun 16 2022 at 09:51):match prf I with end should work then
Gaëtan Gilbert (Jun 16 2022 at 09:51):ie full code
Definition isNone {A:Type} (x:option A) : Prop :=
match x with
| None => True
| Some _ => False
end.
Definition isSome {A:Type} (x:option A) : Prop := not (isNone x).
Definition getSome_prf {A:Type} (x:option A) : isSome x -> A :=
match x with
| Some x => fun _ => x
| None => fun prf => match prf I with end
end.
One thing you should be warned about this approach mixing programs and proofs (the isSome part) is that you can have multiple proofs of isSome x that won't be convertible/definitionally equal (e.g. take two such proofs as argument) and that will bite you when trying to prove theorems on programs using getSome_prf.
With your approach with Prop, you can still prove that all such proofs are propositionally equal (you can show that if p q : isSome x then p = q).
If you use the boolean version you can reuse some standard function because bool has decidable equality, so by Hedberg theorem it verify UIP (from which the previous statement is immediate).
A third solution that I prefer these days (but more advanced) is to have isSome land in SProp so that any two proofs are definitionally equal by construction.
Gaëtan Gilbert (Jun 16 2022 at 09:56):With your approach with Prop, you can still prove that all such proofs are propositionally equal (you can show that if p q : isSome x then p = q).
nope, because it's defined as not so funext gets in the way
Kenji Maillard (Jun 16 2022 at 10:03):oups, Indeed you need to define isSome primitively (in a way similar to isNone)
Kenji Maillard (Jun 16 2022 at 10:03):So the warning should be taken even more seriously :)
Julin S (Jun 16 2022 at 10:06):This problem won't be there if isSome returned bool, right?
Julin S (Jun 16 2022 at 10:09):And in the prf I part of
| None => fun prf => match prf I with end
prf has type isSome x which ends up being False, right?
So why is it like match prf I with end and not like match prf with end?
Gaëtan Gilbert (Jun 16 2022 at 10:11):prf has type isSome None which reduces to not True ie True -> False
Julin S (Jun 16 2022 at 10:12):Okay, so prf I ends being of type False.
Julin S (Jun 16 2022 at 10:14):And what if isSome returned bool like:
Definition isNoneT {A:Type} (x:option A) : bool :=
match x with
| None => true
| Some _ => false
end.
Definition isSomeT {A:Type} (x:option A) : bool :=
negb (isNoneT x).
How can we do getSome_prf?
Trying
Definition getSome_prf {A:Type} (x:option A) : isSomeT x -> A
gave error saying isSomeT x part needed to Set/Prop/Type.
Gaëtan Gilbert (Jun 16 2022 at 10:15):then you need isSomeT x = true when used as a type
Julin S (Jun 16 2022 at 10:17):So the proof for None part would be false = true.
Gaëtan Gilbert (Jun 16 2022 at 10:17):yes
and you have a lemma somewhere that says false = true -> False
Julin S (Jun 16 2022 at 10:23):How would we define getSome_prf with this?
Definition getSome_prf {A:Type} (x:option A)
: isSomeT x = true -> A :=
match x with
| Some x => fun _ => x
| None => fun prf => _
end.
Would it be better to define it in proof mode?
How can we leave holes and fill in later? Was it using refine?
With Program coq somehow figured made the proof by itself, though.
Julin S (Jun 16 2022 at 12:42):Could functions likegetSome_prf be considered examples of 'proof carrying code'?
Paolo Giarrusso (Jun 16 2022 at 14:22):Possibly not, but the idea is similar. The style has enough problems in Coq that many recommend beginners to avoid it.
Paolo Giarrusso (Jun 16 2022 at 14:24):This thread already contains a few tips on pitfalls to account for, but there are probably more.
Paolo Giarrusso (Jun 16 2022 at 14:28):OTOH, _all of the functions used here_ are decidable — instead of
Definition p1 (b:nat->option nat) (n1 n2:nat) : Prop :=
forall n:nat,
(n1 < n < n2) -> (* andb (Nat.ltb n1 n) (Nat.ltb n n2) *)
(b n) = None. (* (isNone (b n)) *)
you can write something like this (I might be using stdpp):
Definition p1b (b:nat->option nat) (n1 n2:nat) : bool :=
forallb (fun n => isNone (b n)) (seq n1 (n2 - n1)).
and prove p1b reflects p1.
Gaëtan Gilbert (Jun 16 2022 at 14:29):do you mean isNone instead of = None?
Paolo Giarrusso (Jun 16 2022 at 14:40):thanks, fixed
Gaëtan Gilbert (Jun 16 2022 at 14:41):forallb and seq are both in stdlib List.v
Julin S (Jun 18 2022 at 18:10):Thanks! I think forallb, existsb and seq can help. But still couldn't finish it.
I tried making the functions with them.
For simplicity, I am considering the case where the return value of the main function (fn) is None. Some value is returned via an else clause.
(That means p0, p1 aren't needed).
Definition p2 (bval cval:option nat) : bool :=
andb (isNoneT bval) (isNoneT cval).
Definition p3 (x1 x2:nat) (b:nat->option nat) : bool :=
forallb (fun x:nat => isSomeT (b x))
(seq x1 (x2-x1)).
Section sec_sn.
Variable a b c : nat -> option nat.
Definition Sn (x:nat) : bool :=
forallb
(fun x':nat =>
(eqSome (a x') (Some (x-x'))) &&
(p2 (b x') (c x')) && (p3 x' x b)
)%bool
(seq 0 (x-1)).
End sec_sn.
Using this, I tried defining the main function:
Fixpoint fn (a b:nat->option nat) : nat -> option nat :=
fun x:nat =>
let snval:bool := (Sn a b (fn a b) x) in
if snval then None
else (Some 1).
But ran into problem in making the recursion happen on a smaller argument (primitive recursion).
Cannot guess decreasing argument of fix.
How can I get around that?
Or could this be expressed differently?
Julin S (Jun 18 2022 at 18:11):fn is supposed to return option nat.
Julin S (Jun 18 2022 at 18:23):Helper functions used:
Definition eqSome (a b:option nat):bool :=
match a, b with
| Some a', Some b' => Nat.eqb a' b'
| _, _ => false
end.
Definition isNoneT {A:Type} (x:option A) : bool :=
match x with
| None => true
| Some _ => false
end.
Definition isSomeT {A:Type} (x:option A) : bool := negb (isNoneT x).
And p0 and p1 (not used):
Definition p0 (x:nat) (b c:nat->option nat) : bool :=
andb (isSomeT (b x)) (isSomeT (c x)).
Definition p1 (x1 x2:nat) (b:nat->option nat) : bool :
forallb (fun x:nat => isNoneT (b x))
(seq x1 (x2-x1)).
well-founded recursion might be helpful as a last resort, but you should probably make sure that fn is correct first... the recursion you've written is pretty strange (and probably exponential). If the scheme is intended, you might be able to first generate the call tree as an inductive tree (by structural recursion on n), then proceed by structural recursion on the generated tree
Paolo Giarrusso (Jun 18 2022 at 23:29):(but you did warn us this was strange)
Julin S (Jun 20 2022 at 04:29):You mean by making a new inductive type?
Julin S (Jun 20 2022 at 05:16):Can CoInductive types be of any help?
Paolo Giarrusso (Jun 20 2022 at 10:34):Coinductives help represent infinitely deep trees, which shouldn't be necessary?
Last updated: Apr 20 2024 at 10:02 UTC