Hello everybody,
Here is a beginner’s question: general speaking, I’d like to define a type that is a “restriction/subtype” of some other inductive type.
I have already been wading through a lot of material as to the several ways this can actually be approached: I am specifically after the simplest possible “structural” solution.
Here is an attempt where I am trying to use a “side condition” (as e.g. coq-elpi says that they restrict compound terms to positive literals this way, if I read that correctly), but I have not been able to find a way to make the extra-hypothesis be somehow checked/filled automatically:
Inductive Nat : Set :=
| NZ : Nat
| NS (n : Nat) : Nat.
Definition isSucc (n : Nat) : Prop :=
n <> NZ.
Inductive oper : Set :=
| Pos (n : Nat)
(H : isSucc n) : oper
| Neg (o : oper) : oper.
Lemma isSucc_NS :
forall (n : Nat), isSucc (NS n).
Proof. discriminate. Qed.
(* I have tried this but it does not help to my purpose. *)
#[export] Hint Resolve isSucc_NS : oper.
Arguments Pos n {H}.
(* I'd like the 3rd argument to have a "default" such that this rather fails. *)
Check (Pos NZ) : oper.
(* Pos NZ : oper
: oper
where
?H : [ |- isSucc NZ] *)
And I have not posted another attempt of mine, where I rather use two distinct types and coercion: that works but then I have some redundancy of constructors, so I should rather find a way to hide a constructor / make it private to a module, etc. etc…
I hope the above at least makes the problem/my intent clear enough, but of course feel free to ask for clarifications.
Suggestions and comments very welcome.
Thank you (and thanks for Coq, the whole community, great stuff indeed!),
Julio
The issue with you current approach is that, by default, Coq does not try to automatically solve existential variables created when type-checking a term (here, the ?H variable that is created when checking (Pos NZ). You can, however, instruct Coq to do so, using so-called “tactics in terms”. In your case, you can do the following:
Notation "'Pos'' n" := (Pos n (H := ltac:(solve [eauto with oper]))) (at level 0).
Check (Pos' (NS NZ)) : oper.
Fail Check (Pos' NZ) : oper.
This defines a new notation Pos', which calls Pos, but crucially uses the tactic eauto with oper to try and fill the implicit argument. As the next line shows, this now correctly fills in the missing argument, if possible. As the last one shows, using solve forces the term to fail if the tactic is not able to fill in the hole.
Not that it is important that Pos' is defined as a notation, as this means the type-checking of the right-hand side, and so the subsequence evaluation of the tactic, will only happen when the notation is used, ie when Pos' is applied to a concrete value. Contrast this with the failing
Fail Definition Pos' n := Pos n (H := ltac:(solve [eauto with oper])).
which tries to use the tactic at definition time to derive the unprovable isSucc_NS n.
1 Like
Hi Meven,
Thanks very much, notation with ltac opens scenarios I had not yet imagined…
That said, I may have shown too simplified an example: indeed, I have been playing with your suggestion and I immediately run into another roadblock.
The fact is my goal is not just to construct those terms, but also to use the “restricted type” (call it [Succ]) as an actual type, as in:
Inductive oper : Set :=
| Pos (n : Succ) : oper
| Neg (o : oper) : oper.
I won’t bother you with my further attempts and ruminations (at least not until I have something new to show [and, I am still playing with it]), though I must say that I am in fact not seeing a way to achieve the above with / along the lines of (just?) notation.
Julio
Eventually I am thinking the working solution I had mentioned, with two inductive types, is in fact more along the lines of what I am after. I was perplexed by some “redundancy” (comments in the code below), but maybe, after all, the fact that an extra constructor appears is indeed the simplest “structural” thing one can do…
No? I’d rather not agonize too long over this, but any further advice or comments still very welcome.
Require Import List.
Module IndTest_2.
Import ListNotations.
Inductive tree : Set :=
| Leaf : tree
| Node (ts : list tree) : tree.
(* [parn] is a type! the *drawback* is that a constructor
(an extra piece of term structure) is introduced to
"just" express a restriction on [tree] terms. *)
Inductive parn : Set :=
| Parn (ts : list tree) : parn.
(* Coercion quite mitigates said drawback. *)
Coercion parn_to_tree (p : parn) : tree :=
match p with Parn ts => Node ts end.
(* Ex.1 term construction with coercion ******** *)
(* Still don't quite like e.g. the first two here:
there should be only one way to write things! *)
Check (Node [Node []]) : tree. (*!*)
Check (Parn [Node []]) : tree. (*!*)
Check (Parn [Node []]) : parn.
Fail Check (Parn [Parn []]).
(* Ex.2 use of the "restricted" type ******** *)
Inductive pseq : Set :=
| Base (p : parn) : pseq
| Succ (p : parn) (ps : pseq) : pseq.
Fail Check (Base Leaf).
Fail Check (Base (Node [])).
Check (Base (Parn [])) : pseq.
Check (Base (Parn [Leaf])) : pseq.
(* Ex.3 function extension from coercion ******** *)
Definition tree_card (t : tree) : nat :=
match t with
| Leaf => 0
| Node ts => length ts
end.
Compute (tree_card Leaf). (*=0*)
Compute (tree_card (Node [])). (*=0*)
Compute (tree_card (Node [Leaf])). (*=1*)
Compute (tree_card (Parn [])). (*=0*)
Compute (tree_card (Parn [Leaf])). (*=1*)
End IndTest_2.
Julio
Here is variant of my proposed “solution” (previous post) which is maybe even better, where parn is defined with a side-condition, so avoiding code duplication, then indeed leveraging notation. It seems to me it even addresses my anyway dubious concerns with the previous solution, but I am still a rookie with Coq…
P.S. Except that I am not allowed to use that notation in pattern matching: Invalid notation for pattern. Then I should think whether overall this solution is in fact acceptable/worth it.
Require List.
Module IndTest_3.
Import List.
Import ListNotations.
Inductive tree : Set :=
| Leaf : tree
| Node (ts : list tree) : tree.
Definition isNode (t : tree) : Prop :=
t <> Leaf.
Lemma Node_is_Node :
forall (ts : list tree), isNode (Node ts).
Proof. discriminate. Qed.
Inductive parn : Set :=
| Parn' (t : tree) (H : isNode t) : parn.
Notation "'Parn' ts" :=
(Parn' (Node ts) (Node_is_Node ts))
(at level 0).
Coercion parn_to_tree (p : parn) : tree :=
match p with Parn' t _ => t end.
(* Ex.1 term construction with coercion ******** *)
(* can't complain about these, can we: *)
Check (Parn' (Parn' _ _) _) : tree.
Check (Parn' (Parn' _ _) _) : parn.
Check (Parn []) : parn.
Check (Parn [Leaf]) : parn.
Check (Parn [Node []]) : parn.
Fail Check (Parn [Parn []]).
(* Ex.2 use of the "restricted" type ******** *)
Inductive pseq : Set :=
| Base (p : parn) : pseq
| Succ (p : parn) (ps : pseq) : pseq.
Fail Check (Base Leaf).
Fail Check (Base (Node [])).
Check (Base (Parn [])) : pseq.
(* Ex.3 function extension from coercion ******** *)
Definition tree_card (t : tree) : nat :=
match t with
| Leaf => 0
| Node ts => length ts
end.
Compute (tree_card Leaf). (*=0*)
Compute (tree_card (Node [])). (*=0*)
Compute (tree_card (Node [Leaf])). (*=1*)
Compute (tree_card (Parn [])). (*=0*)
Compute (tree_card (Parn [Leaf])). (*=1*)
End IndTest_3.