Proof

[Daniel Gavrila]

Hi ,

n: Fin 16

m :Nat 

m = div n 4

Is it possible to proof that m in fact is a Fin 4 ?

Best regards,

Daniel

[Ohad Kammar]

Dear Daniel,

In Idris2, the `contrib` package has some building blocks that can help you:

Data.Nat.Division.boundModNatNZ : (numer, denom : Nat) -> (0 denom_nz : NonZero denom) -> (modNatNZ numer denom denom_nz) `LT` denom

and

Data.Nat.Division.DivisionTheorem : (numer : Nat) -> (denom : Nat) -> (0 prf1 : NonZero denom) -> (0 prf2 : NonZero denom) -> numer = modNatNZ numer denom prf1 + (divNatNZ numer denom prf2 * denom)

which you can use to prove that `16 > n = r + m * 4 >= m * 4`.

You will then need to prove this implies `4 > m`: I think this monotonicity is currently missing from the standard library.

Then you can use `Data.Fin.Extra.natToFinLTE` to get a value of type `Fin 4`.

Yours,

Ohad.

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/8d732d57-be6d-417b-9e1d-6c7ee813d95en%40googlegroups.com.

[Daniel Gavrila]

Dear Ohad,

many thanks for your detailed advice. I will see how far can I go ...

Best regards,

Daniel