How do you operate on dependent pairs in a proof?

This is a follow up to this question. Thanks to Kwartz I now have a state of the proposition if b divides a then b divides a * c for any integer c, namely:

alsoDividesMultiples : (a, b, c : Integer) ->
                       DivisibleBy a b ->
                       DivisibleBy (a * c) b

Now, the goal has been to prove that statement. I realized that I do not understand how to operate on dependent pairs. I tried a simpler problem, which was show that every number is divisible by 1. After a shameful amount of thought on it, I thought I had come up with a solution:

-- All numbers are divisible by 1.
DivisibleBy a 1 = let n = a in
  (n : Integer ** a = 1 * n)

This compiles, but I was had doubts it was valid. To verify that I was wrong, it changed it slightly to:

-- All numbers are divisible by 1.
DivisibleBy a 1 = let n = a in
  (n : Integer ** a = 2 * n)

This also compiles, which means my "English" interpretation is certainly incorrect, for I would interpret this as "All numbers are divisible by one since every number is two times another integer". Thus, I am not entirely sure what I am demonstrating with that statement. So, I went back and tried a more conventional way of stating the problem:

oneDividesAll : (a : Integer) ->
                (DivisibleBy a 1)
oneDividesAll a = ?sorry

For the implementation of oneDividesAll I am not really sure how to "inject" the fact that (n = a). For example, I would write (in English) this proof as:

We wish to show that 1 | a. If so, it follows that a = 1 * n for some n. Let n = a, then a = a * 1, which is true by identity.

I am not sure how to really say: "Consider when n = a". From my understanding, the rewrite tactic requires a proof that n = a.

I tried adapting my fallacious proof:

oneDividesAll : (a : Integer) ->
                (DivisibleBy a 1)
oneDividesAll a = let n = a in (n : Integer ** a = b * n)

But this gives:

   |
12 | oneDividesAll a = let n = a in (n : Integer ** a = b * n)
   |                   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of oneDividesAll with expected type
        DivisibleBy a 1

Type mismatch between
        Type (Type of DPair a P)
and
        (n : Integer ** a = prim__mulBigInt 1 n) (Expected type)

Any help/hints would be appreciated.

Solution

First off, if you want to prove properties on number, you should use Nat (or other inductive types). Integer uses primitives that the argument can't argue further than prim__mulBigInt : Integer -> Integer -> Integer; that you pass two Integer to get one. The compiler doesn't know anything how the resulting Integer looks like, so it cannot prove stuff about it.

So I'll go along with Nat:

DivisibleBy : Nat -> Nat -> Type
DivisibleBy a b = (n : Nat ** a = b * n)

Again, this is a proposition, not a proof. DivisibleBy 6 0 is a valid type, but you won't find a proof : Divisible 6 0. So you were right with

oneDividesAll : (a : Nat) ->
                (DivisibleBy a 1)
oneDividesAll a = ?sorry

With that, you could generate proofs of the form oneDividesAll a : DivisibleBy a 1. So, what comes into the hole ?sorry? :t sorry gives us sorry : (n : Nat ** a = plus n 0) (which is just DivisibleBy a 1 resolved as far as Idris can). You got confused on the right part of the pair: x = y is a type, but now we need a value – that's what's your last error cryptic error message hints at). = has only one constructor, Refl : x = x. So we need to get both sides of the equality to the same value, so the result looks something like (n ** Refl).

As you thought, we need to set n to a:

oneDividesAll a = (a ** ?hole)

For the needed rewrite tactic we check out :search plus a 0 = a, and see plusZeroRightNeutral has the right type.

oneDividesAll a = (a ** rewrite plusZeroRightNeutral a in ?hole)

Now :t hole gives us hole : a = a so we can just auto-complete to Refl:

oneDividesAll a = (a ** rewrite plusZeroRightNeutral a in Refl)

A good tutorial on theorem proving (where it's also explained why plus a Z does not reduce) is in the Idris Doc.