Subtype axioms

[chdoc]

As discussed, it would be nice to tag operators and axioms in certain abstract theories as non-instantiable. For Subtype, this could look as follows:

type T.
pred P : T.

axiom P_nonempty : exists x, P x.

generate type sT. 

generate op insub : T  -> sT option.
generate op val : sT -> T.

generate axiom insubN (x : T): !P x => insub x = None.
generate axiom insubT (x : T):  P x => omap val (insub x) = Some x.

generate axiom valP (x : sT): P (val x).
generate axiom valK: pcancel val insub.

(* rest of the Subtype theory ... *)

The idea is that one can check once (when writing the theory) that the generated collection of operators and axioms is consistent for all instances (that validate the non-generated axioms) and thereby facilitate the use of proof* everywhere else.

Of course, we could implement quotients using choice and subtypes, so this may be the only instance we ever need. IIUC, that's what HOL systems tend to do. So implementing the typedef from Isabelle/HOL is another option.

[strub]

You might be interested by this:

theory T.
axiom [trusted] A : false.
end T.

clone T as U
  proof *[-trusted].

[chdoc]

After a bit of thinking and reading about this, maybe it would be preferable (in particular safer) to implement something akin to the HOL typedef mechanism described for instance in Sect. 2.2 of From Types to Sets by Local Type Definition in Higher-Order Logic.

My main issue with the "trusted axiom" approach is that there is no way to ensure that people won't clone subType with concrete instantiations for val and insub without ever seeing the (then inconsistent) trusted axioms. IIUC, one way or another, we need to be able to create theories with abstract operators that cannot be instantiated during cloning.

Also, I don't think we need more than a typedef. We generally assume a choice operator (aka Hilbert's epsilon-operator), so we can define quotient types as the subtype of (canonical) representatives for equivalence classes.

The aforementioned paper also proposes a variant of typedef that can be used inside proofs. I think this is something that we might want to consider at a later point.

@strub @bgregoir @gbarthe What are your thoughts on this?

[bgregoir]

My impression, is that the problem will be only for the subtype theory. I think, we should provide a simple patch such that we can do a local clone of subtype without problem. Then, we should work on how to have a proper definition of subtype in EC (without need of that theory).

[chdoc]

At the very least, if we tag some of the axioms in subType to not show up in proof*, we also need a way to tag the operators val and insub as uninstantiable. Otherwise, people can (accidentally) introduce (almost) impossible to detect inconsistencies.

[chdoc]

@strub @fdupress @bgregoir This has been dormant for a while. If I recall correctly, tagging ops in a theory as uninstantiable was something that was asked for in Porto for some unrelated reason. If we ensure that val and insub are kept abstract, then suppressing the axioms should be fine.

Incidentally, I think that the current way to handle non-emptiness is suboptimal. This should actually always be proved by the user. But without knowing what the witness of the sT is it's hard to define its preimage as an op (without using choice).

[dominique-unruh]

@chdoc I wrote a replacement for Subtype that alleviates the problem by using several tricks:

• val and insub are not unspecified operators, but defined (via choiceb as "some suitable val and insub"). This makes sure that they cannot be overwritten.
• The only axiom is that the predicate P is inhabited.
• The type sT is also defined, and hence cannot be overwritten. It is defined as a thin wrapper around a type called do_not_use_this_type_or_you_get_unsoundness_admit. While it is technically possible to clone this subtype theory unsoundly (by specifying type do_not_use_this_type_or_you_get_unsoundness_admit = ... during clone), the name makes it unlikely that people do so.
• The fact that there is a bijection between do_not_use_this_type_or_you_get_unsoundness_admit and P is axiomatized, but using lemma ... admit. qed. instead of axiom .... This ensures that clone ... proof * does not require us to prove the existence of this bijection.
• Instead, there is an axiom inhabited saying that P is inhabited. It is not actually used but it ensures that one cannot accidentally instantiate an empty Subtype.

With these changes, one can create subtypes without getting unprovable proof obligations. (The existing mechanism makes it impossible to soundly instantiate many theories that internally use Subtype. E.g., clone ZModP.ZModRing ... proof * requires us to prove the unprovable Subtype axioms, but without proof *, we might not show the important p >= 2 axiom. This is proof of false waiting to happen...) At the same time, everything is sound as long as one follows the rule always to have a proof * when cloning in a non-abstract theory (imho, EasyCrypt should enforce that, or at least make it a strong default), and does not refer to do_not_use_this_type_or_you_get_unsoundness_admit directly while cloning.

With my Subtype replacement (SafeSubtype.eca.txt), one can declare subtypes as follows:

clone SafeSubtype as ST with
  type T = int, 
  op P = fun x:int, 0 <= x
proof *.
realize inhabited.
  exists 0. trivial.
qed.

The theory is designed to be a drop-in replacement for the existing Subtype. It exports the same ops, types, and lemmas.

Main disadvantage: The theory contains an admit. But I think if it's in the stdlib (instead of the existing Subtype), and the admit get a clear comment that it is ok because of the axioms inhabited, then that should be OK. (At least till a builtin subtype command comes along.)

I strongly vote for including it (or something similar) so that we can finally have the rule that all axioms should always be proven. (See also https://github.com/EasyCrypt/easycrypt/issues/331#issuecomment-1411733326)

[strub]

Hi @dominique-unruh. Could you create a PR so that we see what breaks in the standard library?

[fdupress]

One very minor thing to keep in mind (not to stop this change, but to enable it with minimal loss elsewhere) is that defining the injection and projection in all subtypes will likely cause issues like those that arose from doing the same in a specific one ('a distr) last year: the SMT lemma selection is going to suddenly pull in a whole lot more theory that was previously hidden by abstraction.

It might make sense, for now, to make sure that all subtype instantiations in the stdlib are marked as much as possible with nosmt. We can return to working on switching the default independently.

[dominique-unruh]

@strub I'm trying to make the PR (and see where the stdlib breaks) but I run into a mystery and am not sure whether it's intended or a bug.

pred x (c:bool) = true.
op y = x.

fails but

op x (c:bool) = true.
op y = x.

succeeds. In general, it seems that preds can never be part of ops. Is that intentional?

From looking at the reference manual, I don't see any difference between ops and preds (except that the type annotations are written a bit differently).

It's a problem because it means in my Subtype, P has to be an op. But if it's an op, then it will need to be instantiated with ops. But inductive ispoly in Poly.ec is a pred, and I don't see how to make it an op because inductive seems to produce preds.

[dominique-unruh]

@fdupress

It might make sense, for now, to make sure that all subtype instantiations in the stdlib are marked as much as possible with nosmt. We can return to working on switching the default independently.

How does one do that? I only know how to do it to lemmas, but not to theories as a whole. Ideally, we would like to add nosmt to the definitions of val and insub but I don't know if that's possible.

[alleystoughton]

@fdupress

It might make sense, for now, to make sure that all subtype instantiations in the stdlib are marked as much as possible with nosmt. We can return to working on switching the default independently.

How does one do that? I only know how to do it to lemmas, but not to theories as a whole. Ideally, we would like to add nosmt to the definitions of val and insub but I don't know if that's possible.

That one's easy:

op nosmt x : int = 3 + 4.

[fdupress]

Yes-ish: you can't add a nosmt annotation when cloning, so the way you'd need to do it is to first define your op tagged as nosmt, then use it in cloning. Perhaps don't do it and let's see if anything blows up because of the size of SMT contexts.

As for the pred vs op issue, this will count as "something that breaks in the stdlib" and that we need to think hard about sorting out. Easy and dirty fix is to make inductive define an op instead (after thinking about how that impacts a whole bunch of things), but doing this more systematically might also fit current code simplification efforts.

[alleystoughton]

I remember P-Y explaining to me why getting rid of preds entirely would require some major refactoring, but I can't remember (and it must have been on slack).

[dominique-unruh]

@strub I made a pull request. Minor fixes were needed, see my comment in the PR.

[dominique-unruh]

@strub I'm trying to make the PR (and see where the stdlib breaks) but I run into a mystery and am not sure whether it's intended or a bug.

I got around this (it turns out in Poly.ec, the inductive predicate didn't really need to be an inductive one, since it used the inductive predicate in a degenerate case with only one case and no recursion). Stdlib and examples now work.

[strub]

I remember P-Y explaining to me why getting rid of preds entirely would require some major refactoring, but I can't remember (and it must have been on slack).

This is because we have this (now artificial since expressions can contain non-executable constructions) distinction between expressions & formulas.

Now, last time I spoke about this with Benjamin, we realized that operators body could contain formula without having to do a heavy refactoring (having formulas in the RHS of the assignment instruction would be a totally different story). This is something that could be done once Cameron is done with the refactoring of substitutions.

[strub]

Yes-ish: you can't add a nosmt annotation when cloning, so the way you'd need to do it is to first define your op tagged as nosmt, then use it in cloning. Perhaps don't do it and let's see if anything blows up because of the size of SMT contexts.

I think that this should be part of the reflexion around the new behavior of the smt/nosmt annotations.

[strub]

Reopening the issue. The current subtype implementation is a nightmare w.r.t. pretty-printing: all subtypes are named sT and it is hard to understand. I propose to implement Christian ideas.