Proof derivation and functional relation (deterministic)

Google Group
1

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.

2

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

3

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.

4

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

.

5

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] voidOn Monday, December 21, 2015 at 3:55:30 AM UTC-5, Yannick Duchêne wrote:

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))
…

6

[…]
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