Proof derivation and functional relation (deterministic)

[Yannick Duchêne]

A similar question may rise about functions in the large, this is just that I am wondering about it, in the context of proofs.

I wonder how I can check or proof that if I can derive a proof of B from a proof of A, then for a given proof of A (that is, its exact expression with indexes), I can derive only one proof of B (the same, I mean its exact expression with indexes).

Say proofs are like functions, then this is about how to check or prove, a proof function is deterministic and there are no possible arbitrary choices, which may make the result vary.

Some samples may tell better. I expose four cases (then a fifth case about something else related). For all of these four cases, I purposely use the same `prval` expressions to check and show some things. All four cases uses two `dataprop` named R and E (which stands for Representation and Entity).

 * The first two cases are examples of what I want to avoid.

 * The next two cases are examples of what is OK. I don't know how to prove these latter two cases are OK.

// 1) A case where from any R one can derive any E
// ===============================================

sortdef r = int
sortdef e = int

dataprop R(i:r) =
| R1(i)

dataprop E(i:e) =
| E1(i) of [j:r] R(j)

prval pf:E(0) = E1(R1:R(0))
prval pf:E(0) = E1(R1:R(1))
prval pf:E(0) = E1(R1:R(2))
prval pf:E(1) = E1(R1:R(0))
prval pf:E(1) = E1(R1:R(1))
// And so on, whatever one wants …

// 2) A case where from one R one can derive multiple E
// ====================================================

sortdef r = int
sortdef e = int

dataprop R(i:r) =
| R1(i)

dataprop E(i:e) =
| E1(i) of R(i / 2)

prval pf:E(0) = E1(R1:R(0))
// Constraint error: prval pf:E(0) = E1(R1:R(1))
// Constraint error: prval pf:E(0) = E1(R1:R(2))
prval pf:E(1) = E1(R1:R(0))
// Constraint error: prval pf:E(1) = E1(R1:R(1))

// 3) A case where from one R one can derive only one E
// ====================================================

sortdef r = int
sortdef e = int

dataprop R(i:r) =
| R1(i)

dataprop E(i:e) =
| E1(i) of R(i)

prval pf:E(0) = E1(R1:R(0))
// Constraint error: prval pf:E(0) = E1(R1:R(1))
// Constraint error: prval pf:E(0) = E1(R1:R(2))
// Constraint error: prval pf:E(1) = E1(R1:R(0))
prval pf:E(1) = E1(R1:R(1))

// 4) Another case where from one R one can derive only one E
// ==========================================================
//
// However, one E may be derived from multiple R.

sortdef r = int
sortdef e = int

dataprop R(i:r) =
| R1(i)

dataprop E(i:e) =
| E1(i / 2) of R(i)

prval pf:E(0) = E1(R1:R(0))
prval pf:E(0) = E1(R1:R(1))
// Constraint error: prval pf:E(0) = E1(R1:R(2))
// Constraint error: prval pf:E(1) = E1(R1:R(0))
// Constraint error: prval pf:E(1) = E1(R1:R(1))

I naively though about something like this:

extern prfn f():
  [r1, r2: r; e1, e2: e; ~(r1 == r2) || (e1 == e2)]
  (R(r1) -> E(e1), R(r2) -> E(e2))

which would be supposed to mean: for any two functions deriving an R from an E, then r1 == r2 implies e1 == e2.

Unfortunately, even the first case allows to prove it, which shows this cannot ensure the deterministic functional relation I would like to be able to prove or check. I'm repeating the first case, to remind, with the proof added at the end:

// 1) A case where from any R one can derive any E
// ===============================================

sortdef r = int
sortdef e = int

dataprop R(i:r) =
| R1(i)

dataprop E(i:e) =
| E1(i) of [j:r] R(j)

prval pf:E(0) = E1(R1:R(0))
prval pf:E(0) = E1(R1:R(1))
prval pf:E(0) = E1(R1:R(2))
prval pf:E(1) = E1(R1:R(0))
prval pf:E(1) = E1(R1:R(1))
// And so on, whatever one wants …

prfn f():
  [r1, r2: r; e1, e2: e; ~(r1 == r2) || (e1 == e2)]
  (R(r1) -> E(e1), R(r2) -> E(e2)) =
  let
    prfn {i:int} g(r:R(i)): E(i) = E1(R1:R(i))
    stacst i:int
  in (g:R(i) -> E(i), g:R(i) -> E(i)) end

… look at `f`, which is unfortunately provable.

I feel to guess I need quantification over functions. Or is there another way to express it in ATS?

Something different now, while related, as it's about what a result depends on (this one, is obviously applicable to any function too, not just proof functions):

// 5.2) from an axiom from the context
// -----------------------------------

dataprop A =
| A1

dataprop C =
| C1 of C // Bigger than our universe

extern praxi c(): C // Let us be silly

dataprop B =
| B1 of C

prfn b_from_a(pf:A): B = B1(c())
// Not really B from A, rather B from c()!
// How to tell about this proof's dependencies?

This is very important to keep in mind that this:

prfn b_from_a(pf:A): B = B1

… does not necessarily means “B is derivable from A”, as it's too easy to believe (it's particularly important to not miss‑read what one read, when xe read a proof signature).

This case (the fifth case) probably requires manual inspection (may be with the help of a dedicated tool), and this would be OK. However, for the four first cases, I really would like to be able to express it directly.

[gmhwxi]

I think what you need is to define

dataprop ER(i:int, j:int) = ...

ER(i, j) means that E(i) can be derived from R(j)

A proof function of the following type means that
there is at most one i for each j such that ER(i, j) holds:

(ER(i1, j), ER(i2, j)) -> [i1==i2] void

...

[Yannick Duchêne]

Le lundi 21 décembre 2015 17:17:50 UTC+1, gmhwxi a écrit :

I think what you need is to define

dataprop ER(i:int, j:int) = ...

ER(i, j) means that E(i) can be derived from R(j)

It was one of the first idea I had, and though I had to search for better as simple indexes was not looking to me, for more complex expressions, like recursive expressions.

I will resume with this track anyway, as it indeed looks the best. That's what it is for after all, express relations …

 

A proof function of the following type means that
there is at most one i for each j such that ER(i, j) holds:

(ER(i1, j), ER(i2, j)) -> [i1==i2] void

Thanks for this tip.

As a side note for readers, I also tried to quantify over function. That was not ok, as it would need to be of a sort instead of, of a type, and I could not define a function sort for R to E, as E and R are not sort (there is just the broad prop sort, which could not be ok).

Ex. this is possible:

sortdef f = int -> int

Ex. this is not possible:

sortdef g = R -> E

[Yannick Duchêne]

Le lundi 21 décembre 2015 17:58:13 UTC+1, Yannick Duchêne a écrit :

It was one of the first idea I had, and though I had to search for better as simple indexes was not looking to me, for more complex expressions, like recursive expressions.

 (please, read “was not looking good to me”)

While that's feasible. Ex with a simple recursive expression, the index may be the integer resulting from the expression seen as a polynomial (and there may be variations of this). Just that the indexes ranges may be big, and may be this can become an issue for the checker.

[Yannick Duchêne]

Le lundi 21 décembre 2015 17:58:13 UTC+1, Yannick Duchêne a écrit :

[…]

As a side note for readers, I also tried to quantify over function. That was not ok, as it would need to be of a sort instead of, of a type, and I could not define a function sort for R to E, as E and R are not sort (there is just the broad prop sort, which could not be ok).

Ex. this is possible:

sortdef f = int -> int

Ex. this is not possible:

sortdef g = R -> E

Something else, related: as proof type index are classified by sorts, a proof type index cannot be a proof.

Ex, this is not possible:

dataprop A =
| A1

dataprop B(a:A) =
| B1

 

 

[Yannick Duchêne]

Le lundi 21 décembre 2015 17:17:50 UTC+1, gmhwxi a écrit :

I think what you need is to define

dataprop ER(i:int, j:int) = ...

ER(i, j) means that E(i) can be derived from R(j)

A proof function of the following type means that
there is at most one i for each j such that ER(i, j) holds:

(ER(i1, j), ER(i2, j)) -> [i1==i2] void 

For the readers, here is a re-wording of the samples from the initial message, using this idiom. The only difference is that ER is named E, as in the original message. This is indeed convincing (just still don't know if it scales well).

// 1) A case where from any R one can derive any E
// ===============================================

sortdef r = int
sortdef e = int

dataprop R(r:r) =
| R1(r)

dataprop E(e:e, r:r) =
| E1(e, r) of R(r)

prval pf:E(0, 0) = E1(R1:R(0))
prval pf:E(0, 1) = E1(R1:R(1))
prval pf:E(0, 2) = E1(R1:R(2))
prval pf:E(1, 0) = E1(R1:R(0))
prval pf:E(1, 1) = E1(R1:R(1))

// And so on, whatever one wants …

// prfn is_fun {e1,e2:e; r:r} (pf1:E(e1, r), pf2:E(e2, r)): [e1 == e2] void
// Impossible: prvals shows counterexamples with `pf:E(0, 0)` and
// `pf:E(1, 0)`.

// 2) A case where from one R one can derive multiple E
// ====================================================

sortdef r = int
sortdef e = int

dataprop R(r:r) =
| R1(r)

dataprop E(e:e, r:r) =
| E1(r, r/2) of R(r/2)

prval pf:E(0, 0) = E1(R1:R(0))
// Constraint error: prval pf:E(0, 1) = E1(R1:R(1))
// Constraint error: prval pf:E(0, 2) = E1(R1:R(2))
prval pf:E(1, 0) = E1(R1:R(0))
// Constraint error: prval pf:E(1, 1) = E1(R1:R(1))

// prfn is_fun {e1,e2:e; r:r} (pf1:E(e1, r), pf2:E(e2, r)): [e1 == e2] void
// Impossible: prvals shows counterexamples with `pf:E(0, 0)` and
// `pf:E(1, 0)`.

// 3) A case where from one R one can derive only one E
// ====================================================

sortdef r = int
sortdef e = int

dataprop R(r:r) =
| R1(r)

dataprop E(e:e, r:r) =
| E1(r, r) of R(r)

prval pf:E(0, 0) = E1(R1:R(0))
// Constraint error: prval pf:E(0, 1) = E1(R1:R(1))
// Constraint error: prval pf:E(0, 2) = E1(R1:R(2))
// Constraint error: prval pf:E(1, 0) = E1(R1:R(0))
prval pf:E(1, 1) = E1(R1:R(1))

prfn is_fun {e1,e2:e; r:r} (pf1:E(e1, r), pf2:E(e2, r)): [e1 == e2] void =
  let
    prval E1(r):E(e1, r) = pf1
    prval E1(r):E(e2, r) = pf2
  in () end

// 4) Another case where from one R one can derive only one E
// ==========================================================
//
// However, one E may be derived from multiple R.

sortdef r = int
sortdef e = int

dataprop R(r:r) =
| R1(r)

dataprop E(e:e, r:r) =
| E1(r/2, r) of R(r)

prval pf:E(0, 0) = E1(R1:R(0))
prval pf:E(0, 1) = E1(R1:R(1))
// Constraint error: prval pf:E(0, 2) = E1(R1:R(2))
// Constraint error: prval pf:E(1, 0) = E1(R1:R(0))
// Constraint error: prval pf:E(1, 1) = E1(R1:R(1))

prfn is_fun {e1,e2:e; r:r} (pf1:E(e1, r), pf2:E(e2, r)): [e1 == e2] void =
  let
    prval E1(r):E(e1, r) = pf1
    prval E1(r):E(e2, r) = pf2
  in () end

.