Injectivity of inductive types revisited

[nikswamy]

In Issue #349, we see that injective type formers are inconsistent.

In PR #1649, we have a fix to remove injectivity for inductive type definitions, but as remarked there, the fix was unsatisfactory since it only eliminates injectivity on type constructors with type-function parameters whose domain is too large. There are two problems with this:

1. That check was not implemented robustly. E.g., although the following would not have injectivity

type t (a:Type u#0 -> Type u#1) : Type u#0 = | T : t a

The following equivalent variant would---we were not normalizing the type before the check, which is clearly wrong.

let tt = Type u#0 -> Type u#1
type t (a:tt) : Type u#0 = | T : t a

So, this PR first normalizes the type of the parameter.

2. Next, as remarked in Forbidding injectivity of inductive types with parameters that are too large #1649, we should also check the codomain of the type parameter to make sure that it's not too large. In particular, previously, a type such as this would be considered injective:

type bad (a:Type u#1) : Type u#0 = | B : bad a

But, of course, an injective function from Type u#1 -> Type u#0 is nonsense, and with Guido's FStar.Cardinality.Universes you can actually prove that and get False out of it. See BugBoxInjectivity.fst

So, now we also check that the codomain of the type parameter is in a universe less than or equal to the universe of the constructed type.

3. I also supported #push-options "--ext 'compat:injectivity' to retain the behavior prior to the fix, to assist with porting code.

---

The impact of this fix is as follows:

1. See FStar.Constructive.fst: We now need to explicitly destruct constructive equality proofs rather than letting the SMT solver do it, since now the axiom encoding the inversion principle is weaker.

2. The same kind of explicit destruction of proof witnesses also shows up in FStar.WellFounded, FStar.WellFounded.Util, FStar.WellFoundedRelation and FStar.ModifiesGen

In Steel & Pulse, we add meaningless parameters to some inductive types as a type-inference hints, e.g., we have

type ptr (t:Type u#a) : Type0 = { ... ; r: ref t; ... }

although that t is actually unused.

I fixed the Pulse library Pulse.Lib.HigherArray that used this pattern and instead write it like

type ptr' : Type0 = { ... ; r: core_ref; ... }
let ptr (t:Type u#a) = ptr'

retaining the type parameter for better unification in ptr t, but in a shallow, transparent way. This required exposing core_ref and core_ghost_ref etc. in PulseCore, but that was relatively easy.

The same fixes could be applied to Steel.ST.HigherArray, but I did not want to change SteelCore: so, I left this module as is, using
#push-options "--ext 'compat:injectivity'` around the relevant type definitions. Similarly, in Steel.Semantics.Hoare.MST and Steel.ST.EphemeralHashTbl, I used this compat option.

---

We have also been discussing a better long-term fix, which is to simply remove the type parameters altogether from the SMT encoding of a data constructor. That will simplify a lot of things, but is a significant change and will likely pose some challenges in generating the correct patterns for quantifiers, since the parameters will not be present. That change may also open the door to an even more long-standing issue, i.e., #65, subtyping for the parameters of an inductive.

[nikswamy]

Note, we always get injectivity on indices

[nikswamy]

I have merged PRs into zeta, steel, pulse, and everparse for compatibility with this PR.
So, we should be able to merge this without breaking the everest build+zeta.

[aseemr]

This name is another (opened) type parameter? If that type parameter itself is a type in a higher universe, that's ok? As in, returning true here is ok in that case?

[gebner]

Sorry, wrong branch.

[TWal]

FYI, I tested this PR on my projects, and the following sample of code do not typecheck anymore (regardless the fuel/ifuel/z3rlimit):

#set-options "--fuel 0 --ifuel 0"

noeq type map_types = {
  key: eqtype;
  value: Type0;
}

noeq type map_elem (mt:map_types) = {
  key: mt.key;
  value: mt.value;
}

noeq type map (mt:map_types) = {
  key_values: list (map_elem mt)
}

#push-options "--fuel 1 --ifuel 1"
val find_value_aux: #mt:map_types -> key:mt.key -> l:list (map_elem mt) -> Pure (option mt.value)
  (requires True)
  (ensures fun res ->
    match res with
    | None -> True
    | Some value -> List.Tot.memP ({key; value;}) l
  )
let rec find_value_aux #mt key l =
  match l with
  | [] -> None
  | h::t ->
    if h.key = key then
      Some h.value
    else
      match find_value_aux key t with
      | Some res -> Some res
      | None -> None
#pop-options

[nikswamy]

Thanks for the example @TWal

This is indeed a problem, one that could eventually be remedied by what I propose as a long-term fix:

We have also been discussing a better long-term fix, which is to simply remove the type parameters altogether from the SMT encoding of a data constructor.

In the style you have, the parameter mt:map_types is in Type u#1 and my patch then just removes injectivity for it.
So, we can't prove that the record {key; value} has the expected implicit type parameter instantiation.

Here's another way to write it, in a curried style, that does work:

#set-options "--fuel 0 --ifuel 0"

noeq type map_types = {
  key: eqtype;
  value: Type0;
}

noeq type map_elem' (k:eqtype) (v:Type0) = {
  key: k;
  value: v;
}
let map_elem (mt:map_types) = map_elem' mt.key mt.value

noeq type map' (k:eqtype) (v:Type0) = {
  key_values: list (map_elem' k v)
}
let map (mt:map_types) = map' mt.key mt.value

#push-options "--fuel 1 --ifuel 1"
val find_value_aux: #mt:map_types -> key:mt.key -> l:list (map_elem mt) -> Pure (option mt.value)
  (requires True)
  (ensures fun res ->
    match res with
    | None -> True
    | Some value -> List.Tot.memP ({key; value;}) l
  )
let rec find_value_aux #mt key l =
  match l with
  | [] -> None
  | h::t ->
    if h.key = key then
      Some h.value
    else
      match find_value_aux key t with
      | Some res -> Some res
      | None -> None

Would this style work for your code?

[TWal]

Thank you for the workaround! I guess that would work, although a bit inconvenient because the record map_types has more fields.

I do have a few follow-up questions:

• if I understand, the code fails because this PR modifies the injectiveness of the function map_elem from Type u#1 to Type u#0, is that correct?
• if so, why do the code above rely on the injectiveness of map_elem? There is only one instance of map_types?
• the types of map_elem' are still in Type u#1, so why is the workaround doing anything useful?

On a higher-level, I don't understand what is the purpose of that pull-request. Is it because there are still unsoundnesses in the injectivity despite the previous fixes?

[nikswamy]

Type parameter arguments are only projectible when this is_injective_on_tparams is true

[nikswamy]

Generate the base constructor for irrelevance of type param arguments, if not injective on type params

[nikswamy]

This substitution is important: State the typing inversion axiom in terms of the parameters of the type constructor, not the type-parameter arguments of the data constructor---since the latter may be semantically irrelevant.

[mtzguido]

We need to also fix the implementation of equal_data in Syntax.Util, which implements decidable equality (and also simplifications for propositional equality), and assumes injectivity. Otherwise:

type idx : Type u#2 = | A1 | A2

noeq
type test2 (i:idx) : Type u#1 =
  | Mk2 : test2 i

let bad
  (x0 : test2 A1) (x1 : test2 A2) : Lemma False = 
  assert (test2 A1 == test2 A2);
  assert_norm (~(coerce_eq () (Mk2 #A1) == Mk2 #A2));
  ()

let falso () : Lemma False = bad Mk2 Mk2

There may be similar rules in tactics, I'll check.

Also I was suprised to see the equality between test2 A1 and test2 A2 is immediately provable given witnesses for each, is that expected?

[nikswamy]

Thanks @mtzguido! That's a great catch on Syntax.Util.

Also I was suprised to see the equality between test2 A1 and test2 A2 is immediately provable given witnesses for each, is that expected?

Indeed, yes! This is also a surprise and has to do with the encoding of pretyping axiom. I'm looking into it.

[mtzguido]

For the equal_data thing, maybe the Data_ctor attribute should be augmented with a count of the non-injective args? So if we have n non-injective arguments and m remaining injective ones, we can return Equal if everything matches (as usual) but NotEqual only if there is a discrepancy in the remaining m.

The tactics module seems fine.

[nikswamy]

Thanks @mtzguido for your comment above on equality of data constructors and all the help over the past few days ...

My latest set of commits have two additional fixes:

1. For inductive type constructors t a, we usually have a pretyping axiom for inductive types of the form: forall x t a. HasType x (t a) ==> PreType x == t a. However, when t is non-injective in a with a constructor MkT, then we have HasType (MkT a) (t a) and HasType (MkT b) (t b) and MkT a == MkT b. From the pretyping axiom, this would allow us to conclude that PreType (MkT a) == PreType (MkT b) == t a == t b. For non-injective constructors, this axiom is weakened to forall x t a. HasType x (t a) ==> Term_constr_id (PreType x) == Term_constr_id (t a).

2. The eq_tm and eq_t functions, used to compare terms for equality in the normalizer and NBE respectively (and elsewhere), is revised to handle data constructors of non-injective types correctly: In particular when comparing constructor applications, the non-injective parameter arguments are ignored.

Aside from some rlimit and solve restart tweaks, I did not need further changes in the the everest repos