Homework #3

[saucisson]

Homework #3 has been released. Deadline is 15 november 2017 at 23:59.
Look at the course homepage for more information.

[partizanos]

Hello, I am not sure what is expected to write in the TODO of proof_spec.lua file, could you explain it a bit more analytically? Any hints?

[saucisson]

In proof_spec.lua, you have to fill the proof that x+y = y+x, using the constructs that have been defined in theorem.lua. You can look at proofs that have already been done in theorem_spec.lua.

[subrsubrr]

In the transitivity method, in the code, there is a line:

local ok, variables = Adt.Term.equivalence (lhs [2], rhs [1])

. . . which gives ok the value of true if lhs[2] and rhs[1] are equal to each other.
This represents the acknowledgement that in t=t AND t=t``, the second term of the left-hand side (t in this case) and the first term of right-hand side(t in this case) are equivalent. This needs to be so in order for transitivity to be applied. However, substitutivity has no such conditions - there are many AND gates, and they are not dependent on each other - t must be equal to t`, but that is within the clause. There is no relationship between t(n) and t(n+1), for example. The terms between the clauses are independent. So how are we supposed to obtain the variables that are mentioned in the end of the method? Thanks.

[saucisson]

You have to ask yourself: what is the purpose of the variables field, that is returned by every Theorem.* function?

[partizanos]

Question how can we access from in a theorem such as s(0) + x = s(x) lets assume it is t1
to apply substitution on the s(x) to make it s(x+0)
how can we send the variable?

--Trying to substitute:
Theorem.substitution(
      t1,
      t1.variables [Natural.Successor{Natural._x}],
      Natural.Addition { Natural._x, Natural.Zero {} }
    )

--This return value
t1.variables [Natural._x]
--This return nill
t1.variables [Natural.Successor[Natural._x]]

I know it is late just curious...

[partizanos]

And second question the required packages such as adt
where are they in the filesystem? I could not find them within the project folder :/

[saucisson]

The art module is in modelisation-verification/homework/proofs/src/adt/init.lua. You have to run the luacheck, busted, .... commands within modelisation-verification/homework/proofs/, and they should automatically find the modules.

[partizanos]

I wanted to see its inner implementation mostly, busted and luacheck run good indeed :)

[partizanos]

Hello I want to ask if the homework 3 was corrected because in the TP of Friday it was mentioned it would be release in some hours but I have not yet received a correction and I am not sure if it is because my github repo has some problem or because it was not yet released.
Thank you in advance

[saucisson]

Sorry, grades will be pushed in a few days.