diff --git a/docs/proofs/definitional.rst b/docs/proofs/definitional.rst index 1e1b696..15fb189 100644 --- a/docs/proofs/definitional.rst +++ b/docs/proofs/definitional.rst @@ -1,4 +1,5 @@ -In order to understand how to write proofs in Idris I think its worth clarifying some fundamentals, such as, +Before we discuss the details of theorem proving in Idris, we will describe +some fundamental concepts: - Propositions and judgments - Boolean and constructive logic @@ -9,8 +10,9 @@ In order to understand how to write proofs in Idris I think its worth clarifying Propositions and Judgments ========================== -Propositions are the subject of our proofs, before the proof then we can't formally say if they are true or not. If the proof is successful then the result is a 'judgment'. -For instance, if the ``proposition`` is, +Propositions are the subject of our proofs. Before the proof, we can't +formally say if they are true or not. If the proof is successful then the +result is a 'judgment'. For instance, if the ``proposition`` is, +-------+ | 1+1=2 | @@ -28,65 +30,67 @@ Or if the ``proposition`` is, | 1+1=3 | +-------+ -Obviously we can't prove it is true, but it is still a valid proposition and perhaps we can prove it is false so the ``judgment`` is, +we can't prove it is true, but it is still a valid proposition and perhaps we +can prove it is false so the ``judgment`` is, +-------------+ | 1+1=3 false | +-------------+ -This may seem a bit pedantic but it is important to be careful, in mathematics not every proposition is true or false for instance, a proposition may be unproven or even unprovable. +This may seem a bit pedantic but it is important to be careful: in mathematics +not every proposition is true or false. For instance, a proposition may be +unproven or even unprovable. -So the logic here is different from the logic that comes from boolean algebra. In that case what is not true is false and what is not false is true. The logic we are using here does not have this 'law of excluded middle' so we have to be careful not to use it. +So the logic here is different from the logic that comes from boolean algebra. +In that case what is not true is false and what is not false is true. The logic +we are using here does not have this law, the "Law of Excluded Middle", so we +cannot use it. -A false proposition is taken to be a contradiction and if we have a contradiction then we can prove anything, so we need to avoid this. Some languages, used in proof assistants, prevent contradictions but such languages cannot be Turing complete, so Idris does not prevent contradictions. +A false proposition is taken to be a contradiction and if we have a +contradiction then we can prove anything, so we need to avoid this. Some +languages, used in proof assistants, prevent contradictions. -The logic we are using is called constructive (or sometimes intuitional) because we are constructing a 'database' of judgments. - -There are also many other types of logic, another important type of logic for Idris programmers is '``linear logic``' but that's not discussed on this page. +The logic we are using is called constructive (or sometimes intuitional) +because we are constructing a 'database' of judgments. Curry-Howard correspondence -=========================== +--------------------------- -So how to we relate these proofs to Idris programs? It turns out that there is a correspondence between constructive logic and type theory. They are the same structure and we can switch backward and forward between the two notations because they are the same thing. +So how do we relate these proofs to Idris programs? It turns out that there is +a correspondence between constructive logic and type theory. They have the same +structure and we can switch back and forth between the two notations. -The way that this works is that a proposition is a type so this, +The way that this works is that a proposition is a type so... .. code-block:: idris - Idris> 1+1=2 - 2 = 2 : Type + Main> 1 + 1 = 2 + 2 = 2 -is a proposition and it is also a type. This is built into Idris so when an '=' equals sign appears in a function type an equality type is generated. The following will also produce an equality type: + Main> :t 1 + 1 = 2 + (fromInteger 1 + fromInteger 1) === fromInteger 2 : Type + +...is a proposition and it is also a type. The +following will also produce an equality type: .. code-block:: idris - Idris> 1+1=3 - 2 = 3 : Type + Main> 1 + 1 = 3 + 2 = 3 -Both of these are valid propositions so both are valid equality types. But how do we represent true judgment, that is, how do we denote 1+1=2 is true but not 1+1=3. -A type that is true is inhabited, that is, it can be constructed. An equality type has only one constructor 'Refl' so a proof of 1+1=2 is +Both of these are valid propositions so both are valid equality types. But how +do we represent a true judgment? That is, how do we denote 1+1=2 is true but not +1+1=3? A type that is true is inhabited, that is, it can be constructed. An +equality type has only one constructor 'Refl' so a proof of 1+1=2 is .. code-block:: idris onePlusOne : 1+1=2 onePlusOne = Refl -So how can Refl, which is a constructor without any parameters, construct an equality type? If we type it on its own then it can't: - -.. code-block:: idris - - Idris> Refl - (input):Can't infer argument A to Refl, Can't infer argument x to Refl - -So it must pattern match on its return type: - -.. code-block:: idris - - Idris> the (1=1) Refl - Refl : 1 = 1 - -So now that we can represent propositions as types other aspects of propositional logic can also be translated to types as follows: +Now that we can represent propositions as types other aspects of +propositional logic can also be translated to types as follows: +----------+-------------------+--------------------------+ | | propositions | example of possible type | @@ -132,28 +136,39 @@ We can have a type which corresponds to disjunction: There is a built in type called 'Either'. Definitional and Propositional Equalities -========================================= +----------------------------------------- -We have seen that we can 'prove' a type by finding a way to construct a term. In the case of equality types there is only one constructor which is 'Refl'. -We have also seen that each side of the equation does not have to be identical like '2=2'. It is enough that both sides are ``definitionaly equal`` like this: +We have seen that we can 'prove' a type by finding a way to construct a term. +In the case of equality types there is only one constructor which is ``Refl``. +We have also seen that each side of the equation does not have to be identical +like '2=2'. It is enough that both sides are *definitionaly equal* like this: .. code-block:: idris onePlusOne : 1+1=2 onePlusOne = Refl -So both sides of this equation nomalise to 2 and so Refl will type match and the proposition is proved. +Both sides of this equation nomalise to 2 and so Refl matches and the +proposition is proved. -We don't have to stick to terms, can also use symbolic parameters so the following will compile: +We don't have to stick to terms, we can also use symbolic parameters so the +following type checks: .. code-block:: idris varIdentity : m = m varIdentity = Refl -If a proposition/equality type is not definitionaly equal but is still true then it is ``propositionaly equal``. In this case we may still be able to prove it but some steps in the proof may require us to add something into the terms or at least to take some sideways steps to get to a proof. +If a proposition/equality type is not definitionaly equal but is still true +then it is *propositionaly equal*. In this case we may still be able to prove +it but some steps in the proof may require us to add something into the terms +or at least to take some sideways steps to get to a proof. -Especially when working with equalities containing variable terms (inside functions) it can be hard to know which equality types are definitially equal, in this example plusReducesL is '``definitially equal``' but plusReducesR is not (although it is '``propositionaly equal``'). The only difference between them is the order of the operands. +Especially when working with equalities containing variable terms (inside +functions) it can be hard to know which equality types are definitionally equal, +in this example ``plusReducesL`` is *definitionally equal* but ``plusReducesR`` is +not (although it is *propositionaly equal*). The only difference between +them is the order of the operands. .. code-block:: idris @@ -163,69 +178,33 @@ Especially when working with equalities containing variable terms (inside functi plusReducesR : (n:Nat) -> plus n Z = n plusReducesR n = Refl -plusReducesR gives the following error: +Checking ``plusReducesR`` gives the following error: .. code-block:: idris - - + Errors (1) - `-- proof.idr line 6 col 17: - When checking right hand side of plusReducesR with expected type - plus n 0 = n + Proofs.idr:21:18--23:1:While processing right hand side of Main.plusReducesR at Proofs.idr:21:1--23:1: + Can't solve constraint between: + plus n Z + and + n - Type mismatch between - n = n (Type of Refl) - and - plus n 0 = n (Expected type) +So why is ``Refl`` able to prove some equality types but not others? - Specifically: - Type mismatch between - n - and - plus n 0 +The first answer is that ``plus`` is defined by recursion on its first +argument. So, when the first argument is ``Z``, it reduces, but not when the +second argument is ``Z``. -So why is 'Refl' able to prove some equality types but not others? +If an equality type can be proved/constructed by using ``Refl`` alone it is known +as a *definitional equality*. In order to be definitionally equal both sides +of the equation must normalise to the same value. -The first answer is that 'plus' is defined in such a way that it splits on its first argument so it is simple to prove when 0 is the first argument but not the second. So what is the general way to know if Refl will work? - -If an equality type can be proved/constructed by using Refl alone it is known as a ``definitional equality``. In order to be definitinally equal both sides of the equation must normalise to unique values. That is, each step in the proof must reduce the term so each step is effectively forced. - -So when we type 1+1 in Idris it is immediately converted to 2 because definitional equality is built in. +So when we type ``1+1`` in Idris it is immediately reduced to 2 because +definitional equality is built in .. code-block:: idris - Idris> 1+1 - 2 : Integer + Main> 1+1 + 2 In the following pages we discuss how to resolve propositionaly equalies. - -Axiomatic and Constructive Approaches -===================================== - -How should we define types so that we can do proofs on them? In the natural numbers with plus example we could have started by treating it as a group based on the plus operator. So we have axioms: - -- for all x,y : ``x+y=y+x`` -- for all x: ``x + 0 = x = 0 + x`` -- for all x,y,z: ``(x + y) + z = x + (x + z)`` - -Then we can implement '+' so that it respects these axioms (presumably implemented in hardware). - -These are axioms, that is a propositions/types that are asserted to be true without proof. In Idris we can use the 'postulate' keyword - - -.. code-block:: idris - - commutePlus ``postulate``: x -> y -> plus x y = plus y x - -Alternatively we could define the natural numbers based on Zero and Successor. The axioms above then become derived rules and we also gain the ability to do inductive proofs. - -As we know, Idris uses both of these approaches with automatic coercion between them which gives the best of both worlds. - -So what can we learn from this to implement out own types: - -- Should we try to implement both approaches? -- Should we define our types by constructing up from primitive types? - -Proof theory affects these design decisions. - - diff --git a/docs/proofs/index.rst b/docs/proofs/index.rst index 69c5b76..904c524 100644 --- a/docs/proofs/index.rst +++ b/docs/proofs/index.rst @@ -4,9 +4,7 @@ Theorem Proving ############### -A tutorial on theorem proving in Idris. - -NOT YET UPDATED FOR IDRIS 2! +A tutorial on theorem proving in Idris 2. .. note:: @@ -25,6 +23,3 @@ NOT YET UPDATED FOR IDRIS 2! inductive patterns propositional - interactive - interactiveOld - diff --git a/docs/proofs/inductive.rst b/docs/proofs/inductive.rst index 1d954af..3618548 100644 --- a/docs/proofs/inductive.rst +++ b/docs/proofs/inductive.rst @@ -52,13 +52,14 @@ function capturing all such inductive definitions: .. code-block:: idris - nat_induction : (P : Nat -> Type) -> -- Property to show - (P Z) -> -- Base case - ((k : Nat) -> P k -> P (S k)) -> -- Inductive step - (x : Nat) -> -- Show for all x - P x - nat_induction P p_Z p_S Z = p_Z - nat_induction P p_Z p_S (S k) = p_S k (nat_induction P p_Z p_S k) + nat_induction : + (prop : Nat -> Type) -> -- Property to show + (prop Z) -> -- Base case + ((k : Nat) -> prop k -> prop (S k)) -> -- Inductive step + (x : Nat) -> -- Show for all x + prop x + nat_induction prop p_Z p_S Z = p_Z + nat_induction prop p_Z p_S (S k) = p_S k (nat_induction prop p_Z p_S k) Using ``nat_induction``, we can implement an equivalent inductive version of ``plus``: @@ -78,16 +79,16 @@ To prove that ``plus n m = plus m n`` for all natural numbers ``n`` and induction on ``n``, or vice versa. We can sketch an outline of a proof; performing induction on ``n``, we have: -- Property ``P`` is ``\x => plus x m = plus m x``. +- Property ``prop`` is ``\x => plus x m = plus m x``. -- Show that ``P`` holds in the base case and inductive step: +- Show that ``prop`` holds in the base case and inductive step: - - | Base case: ``P Z``, i.e. + - | Base case: ``prop Z``, i.e. | ``plus Z m = plus m Z``, which reduces to | ``m = plus m Z`` due to the definition of ``plus``. - - | Inductive step: Inductively, we know that ``P k`` holds for a specific, fixed ``k``, i.e. - | ``plus k m = plus m k`` (the induction hypothesis). Given this, show ``P (S k)``, i.e. + - | Inductive step: Inductively, we know that ``prop k`` holds for a specific, fixed ``k``, i.e. + | ``plus k m = plus m k`` (the induction hypothesis). Given this, show ``prop (S k)``, i.e. | ``plus (S k) m = plus m (S k)``, which reduces to | ``S (plus k m) = plus m (S k)``. From the induction hypothesis, we can rewrite this to | ``S (plus m k) = plus m (S k)``. diff --git a/docs/proofs/interactive.rst b/docs/proofs/interactive.rst deleted file mode 100644 index f432852..0000000 --- a/docs/proofs/interactive.rst +++ /dev/null @@ -1,296 +0,0 @@ -*************************** -Interactive Theorem Proving -*************************** - -Idris supports interactive theorem proving via elaborator reflection. - -:ref:`elaborator-reflection` is also used to convert high-level Idris code into -the core language and for customising the language. Here we show how to use it -to interactively construct proofs. - -The primary purpose of the elaboration mechanism is to elaborate Idris and so it -is not optimised to work as a proof assistant, however it can interactively -construct proofs as described on this page. - -Elab and Pruviloj Libraries -=========================== - -Elaborator reflection is defined in prelude/Language/Reflection/Elab.idr -and pruviloj is defined in Idris-dev/libs/pruviloj/ - -``Elab`` defines the basics such as: solve, attack, intro, compute, -rewriteWith and others. -``pruviloj`` defines some more advanced derived commands such as: -reflexivity and others. - -To use ``pruviloj`` call Idris with the "-p pruviloj" option and add: - -.. code-block:: idris - - import Pruviloj - import Pruviloj.Induction - -to the top of your file. - -It is useful to get the docs at the REPL by using the ``:doc`` command, and -search the docstrings using ``:apropos``. So to introduce the functions from -Elab and Pruviloj, that we will need for the following example, here are -their docstrings: - -.. code-block:: idris - - *plusReducesZ> :doc solve - Language.Reflection.Elab.Tactics.solve : Elab () - Substitute a guess into a hole. - -.. code-block:: idris - - *plusReducesZ> :doc attack - Language.Reflection.Elab.Tactics.attack : Elab () - Convert a hole to make it suitable for bindings - that is, transform - it such that it has the form ?h : t . h as opposed to ?h : t . f h. - - The binding tactics require that a hole be directly under its binding, - or else the scopes of the generated terms won't make sense. This - tactic creates a new hole of the proper form, and points the old hole - at it. - -.. code-block:: idris - - *plusReducesZ> :doc intro - Language.Reflection.Elab.Tactics.intro : (n : TTName) -> Elab () - Introduce a lambda binding around the current hole and focus on the - body. Requires that the hole be in binding form (use attack). - Arguments: - n : TTName -- the name to use for the argument - -.. code-block:: idris - - *plusReducesZ> :doc compute - Language.Reflection.Elab.Tactics.compute : Elab () - Normalise the goal. - -.. code-block:: idris - - *plusReducesZ> :doc rewriteWith - Language.Reflection.Elab.Tactics.rewriteWith : Raw -> Elab () - Attempt to rewrite the goal using an equality. - - The tactic searches the goal for applicable subterms, and constructs a - context for replace using them. In some cases, this is not possible, - and replace must be called manually with an appropriate context. - - Because this tactic internally introduces a let binding, it requires - that the hole be immediately under its binder (use attack if it might - not be). - -Here is the command from pruviloj that we will need for the example on -this page: - -.. code-block:: idris - - *plusReducesZ> :doc reflexivity - Pruviloj.Core.reflexivity : Elab () - A special-purpose tactic that attempts to solve a goal using Refl. - This is useful for ensuring that goals in fact are trivial when - developing or testing other tactics; otherwise, consider using search. - -Interactive Example: plusReduces -================================ - -One way to write proofs interactively is to write the general *structure* of -the proof, and use the interactive mode to complete the details. -Consider the following definition, proved in :ref:`sect-theorems`: - -.. code-block:: idris - - plusReduces : (n:Nat) -> plus Z n = n - -We’ll be constructing the proof by *induction*, so we write the cases for ``Z`` -and ``S``, with a recursive call in the ``S`` case giving the inductive -hypothesis, and insert *holes* for the rest of the definition: - -.. code-block:: idris - - import Pruviloj - import Pruviloj.Induction - - plusReducesZ' : (n:Nat) -> n = plus n Z - plusReducesZ' Z = ?plusredZ_Z - plusReducesZ' (S k) = let ih = plusReducesZ' k in - ?plusredZ_S - -On running , two global names are created, ``plusredZ_Z`` and -``plusredZ_S``, with no definition. - -.. code-block:: idris - - *theorems> : idris plusReducesZ.idr -p pruviloj - - . / _/___/ /____(_)____ - / // __ / ___/ / ___/ Version 1.2.0 - _/ // /_/ / / / (__ ) http://www.idris-lang.org/ - /___/\__,_/_/ /_/____/ Type :? for help - - Idris is free software with ABSOLUTELY NO WARRANTY. - For details type :warranty. - Holes: Main.plusredZ_S, Main.plusredZ_Z - -This tells us that we have two holes Main.plusredZ_S and Main.plusredZ_Z. We can solve -these separately, ``plusredZ_Z`` is the simplest so we will do that first. - -The ``:elab plusredZ_Z`` command enters interactive elaboration mode, which can be used to -complete the missing definition for plusredZ_Z. - -.. code-block:: idris - - *plusReducesZ> :elab plusredZ_Z - - ---------- Goal: ---------- - {hole_0} : 0 = 0 - -This has been normalised to ``0 = 0`` so now we have to prove that ``0`` equals ``0``, which -is easy to prove by reflexivity from the pruviloj library: - -.. code-block:: idris - - -Main.plusredZ_Z> reflexivity - plusredZ_Z: No more goals. - -This tells us that the proof is complete. We can now leave the interactive mode which -we entered with the ``:elab`` command. We do this with the ``:qed`` command: - -.. code-block:: idris - - -Main.plusredZ_Z> :qed - Proof completed! - Main.plusredZ_Z = %runElab (do reflexivity) - Holes: Main.plusredZ_S - -This gives us a trace of the proof which is ``plusredZ_Z = %runElab (do reflexivity)``. We -can cut & paste this into the hole in the original file. This also tells us that we -have another hole ``Main.plusredZ_S`` remaining. - -This remaining proof is bit more complicated, the following diagram gives an overview: - -|image| - -We approach this remaining proof in the same way by using the ``:elab`` command: - -.. code-block:: idris - - *plusReducesZ> :elab plusredZ_S - - - ---------- Goal: ---------- - {hole_0} : (k : Nat) -> (k = plus k 0) -> S k = S (plus k 0) - -In this case, the goal is a function type, using ``k`` (the argument -accessible by pattern matching) and ``ih`` — the local variable -containing the result of the recursive call. We can introduce these as -assumptions using the ``intro`` tactic twice. The parameter is entered as -a constant of type ``TTName`` which is entered as a backtick with double -braces \`{{ih}}. This gives: - -.. code-block:: idris - - -Main.plusredZ_S> intro `{{k}} - - ---------- Assumptions: ---------- - k : Nat - ---------- Goal: ---------- - {hole_0} : (k = plus k 0) -> S k = S (plus k 0) - -Main.plusredZ_S> intro `{{ih}} - - ---------- Assumptions: ---------- - k : Nat - ih : k = plus k 0 - ---------- Goal: ---------- - {hole_0} : S k = S (plus k 0) - -We know, from the type of ``ih``, that ``k = plus k 0``, so we would -like to use this knowledge to replace ``plus k 0`` in the goal with -``k``. We can achieve this with the ``rewriteWith`` tactic: - -.. code-block:: idris - - -Main.plusredZ_S> rewriteWith (Var `{{ih}}) - - ---------- Assumptions: ---------- - k : Nat - ih : k = plus k 0 - ---------- Goal: ---------- - {hole_0} : S k = S k - -The ``rewriteWith`` tactic takes an equality proof as an argument, and tries -to rewrite the goal using that proof. The ih value is entered as a constant -of type ``TTName`` which is entered as a backtick with double braces `{{ih}} but -``rewriteWith`` requires an expression of type ``Raw``, rather than just a name, -so the Var constructor is used to make a variable. Here, it results in an equality -which is trivially provable using reflexivity: - -.. code-block:: idris - - -Main.plusredZ_S> reflexivity - plusredZ_S: No more goals. - -Main.plusredZ_S> :qed - Proof completed! - Main.plusredZ_S = %runElab (do intro `{{k}} - intro `{{ih}} - rewriteWith (Var `{{ih}}) - reflexivity) - -We can't just cut & paste this into the hole in the original file like this: - -.. code-block:: idris - - import Pruviloj - import Pruviloj.Induction - - %language ElabReflection - - plusReducesZ' : (n:Nat) -> n = plus n Z - plusReducesZ' Z = %runElab (do reflexivity) - plusReducesZ' (S k) = let ih = plusReducesZ' k in - (%runElab (do intro `{{k}} - intro `{{ih}} - rewriteWith (Var `{{ih}}) - reflexivity) - ) - -because this gives the following error: - -.. code-block:: idris - - Idris> :load elabInteractiveEx2.idr - elabInteractiveEx2.idr:10:32: - | - 10 | intro `{{ih}} - | ^ - unexpected "in" - expecting dependent type signature - -However if we put the proof into a separate function like this: - -.. code-block:: idris - - import Pruviloj - import Pruviloj.Induction - - %language ElabReflection - - plusredZ_S : (k : Nat) -> (ih:(k = plus k Z)) -> (S k = S (plus k Z)) - plusredZ_S = %runElab (do intro `{{k}} - intro `{{ih}} - rewriteWith (Var `{{ih}}) - reflexivity) - - plusReducesZ' : (n:Nat) -> n = plus n Z - plusReducesZ' Z = %runElab (do reflexivity) - plusReducesZ' (S k) = let ih = plusReducesZ' k in plusredZ_S k ih - -This then loads [#f1]_ . - -.. [#f1] https://github.com/idris-lang/Idris-dev/issues/4556 - -.. |image| image:: ../image/plusReducesProof.png diff --git a/docs/proofs/interactiveOld.rst b/docs/proofs/interactiveOld.rst deleted file mode 100644 index 671b987..0000000 --- a/docs/proofs/interactiveOld.rst +++ /dev/null @@ -1,169 +0,0 @@ -************************************************************** -DEPRECATED: Interactive Theorem Proving Using Old Tactics Code -************************************************************** - -.. warning:: - The interactive theorem-proving interface documented here has been - deprecated in favor of :ref:`elaborator-reflection`. - -Idris also supports interactive theorem proving via tactics. This -is generally not recommended to be used directly, but rather used as a -mechanism for building proof automation which is beyond the scope of this -tutorial. In this section, we briefly discus tactics. - -One way to write proofs interactively is to write the general *structure* of -the proof, and use the interactive mode to complete the details. -Consider the following definition, proved in :ref:`sect-theorems`: - -.. code-block:: idris - - plusReduces : (n:Nat) -> plus Z n = n - -We’ll be constructing the proof by *induction*, so we write the cases for ``Z`` -and ``S``, with a recursive call in the ``S`` case giving the inductive -hypothesis, and insert *holes* for the rest of the definition: - -.. code-block:: idris - - plusReducesZ' : (n:Nat) -> n = plus n Z - plusReducesZ' Z = ?plusredZ_Z - plusReducesZ' (S k) = let ih = plusReducesZ' k in - ?plusredZ_S - -On running , two global names are created, ``plusredZ_Z`` and -``plusredZ_S``, with no definition. We can use the ``:m`` command at the -prompt to find out which holes are still to be solved (or, more -precisely, which functions exist but have no definitions), then the -``:t`` command to see their types: - -.. code-block:: idris - - *theorems> :m - Global holes: - [plusredZ_S,plusredZ_Z] - -.. code-block:: idris - - *theorems> :t plusredZ_Z - plusredZ_Z : Z = plus Z Z - - *theorems> :t plusredZ_S - plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z - -The ``:p`` command enters interactive proof mode, which can be used to -complete the missing definitions. - -.. code-block:: idris - - *theorems> :p plusredZ_Z - - ---------------------------------- (plusredZ_Z) -------- - {hole0} : Z = plus Z Z - -This gives us a list of premises (above the line; there are none here) -and the current goal (below the line; named ``{hole0}`` here). At the -prompt we can enter tactics to direct the construction of the proof. In -this case, we can normalise the goal with the ``compute`` tactic: - -.. code-block:: idris - - -plusredZ_Z> compute - - ---------------------------------- (plusredZ_Z) -------- - {hole0} : Z = Z - -Now we have to prove that ``Z`` equals ``Z``, which is easy to prove by -``Refl``. To apply a function, such as ``Refl``, we use ``refine`` which -introduces subgoals for each of the function’s explicit arguments -(``Refl`` has none): - -.. code-block:: idris - - -plusredZ_Z> refine Refl - plusredZ_Z: no more goals - -Here, we could also have used the ``trivial`` tactic, which tries to -refine by ``Refl``, and if that fails, tries to refine by each name in -the local context. When a proof is complete, we use the ``qed`` tactic -to add the proof to the global context, and remove the hole from the -unsolved holes list. This also outputs a trace of the proof: - -.. code-block:: idris - - -plusredZ_Z> qed - plusredZ_Z = proof - compute - refine Refl - -.. code-block:: idris - - *theorems> :m - Global holes: - [plusredZ_S] - -The ``:addproof`` command, at the interactive prompt, will add the proof -to the source file (effectively in an appendix). Let us now prove the -other required lemma, ``plusredZ_S``: - -.. code-block:: idris - - *theorems> :p plusredZ_S - - ---------------------------------- (plusredZ_S) -------- - {hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z - -In this case, the goal is a function type, using ``k`` (the argument -accessible by pattern matching) and ``ih`` — the local variable -containing the result of the recursive call. We can introduce these as -premises using the ``intro`` tactic twice (or ``intros``, which -introduces all arguments as premises). This gives: - -.. code-block:: idris - - k : Nat - ih : k = plus k Z - ---------------------------------- (plusredZ_S) -------- - {hole2} : S k = plus (S k) Z - -Since plus is defined by recursion on its first argument, the term -``plus (S k) Z`` in the goal can be simplified, so we use ``compute``. - -.. code-block:: idris - - k : Nat - ih : k = plus k Z - ---------------------------------- (plusredZ_S) -------- - {hole2} : S k = S (plus k Z) - -We know, from the type of ``ih``, that ``k = plus k Z``, so we would -like to use this knowledge to replace ``plus k Z`` in the goal with -``k``. We can achieve this with the ``rewrite`` tactic: - -.. code-block:: idris - - -plusredZ_S> rewrite ih - - k : Nat - ih : k = plus k Z - ---------------------------------- (plusredZ_S) -------- - {hole3} : S k = S k - - -plusredZ_S> - -The ``rewrite`` tactic takes an equality proof as an argument, and tries -to rewrite the goal using that proof. Here, it results in an equality -which is trivially provable: - -.. code-block:: idris - - -plusredZ_S> trivial - plusredZ_S: no more goals - -plusredZ_S> qed - plusredZ_S = proof { - intros; - rewrite ih; - trivial; - } - -Again, we can add this proof to the end of our source file using the -``:addproof`` command at the interactive prompt. diff --git a/docs/proofs/patterns.rst b/docs/proofs/patterns.rst index 58d499e..bc18f33 100644 --- a/docs/proofs/patterns.rst +++ b/docs/proofs/patterns.rst @@ -16,9 +16,9 @@ mapping to Emacs commands. +---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+ | Check type | ``\t`` | ``C-c C-t`` | Show type of identifier or hole under the cursor. | +---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+ -| Proof search | ``\o`` | ``C-c C-a`` | Attempt to solve hole under the cursor by applying simple proof search. | +| Proof search | ``\s`` | ``C-c C-a`` | Attempt to solve hole under the cursor by applying simple proof search. | +---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+ -| Make new definition | ``\d`` | ``C-c C-s`` | Add a template definition for the type defined under the cursor. | +| Make new definition | ``\a`` | ``C-c C-s`` | Add a template definition for the type defined under the cursor. | +---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+ | Make lemma | ``\l`` | ``C-c C-e`` | Add a top level function with a type which solves the hole under the cursor. | +---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+ @@ -36,7 +36,7 @@ declaration: plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n -To create a template definition for the proof, press ``\d`` (or the +To create a template definition for the proof, press ``\a`` (or the equivalent in your editor of choice) on the line with the type declaration. You should see: @@ -64,20 +64,18 @@ in each respective case. Pressing ``\t`` over .. code-block:: idris - m : Nat - -------------------------------------- - plus_commutes_rhs_1 : m = plus m 0 + m : Nat + ------------------------------------- + plus_commutes_rhs_1 : m = plus m Z -Note that ``Z`` renders as ``0`` because the pretty printer renders -natural numbers as integer literals for readability. Similarly, for -``plus_commutes_rhs_2``: +Similarly, for ``plus_commutes_rhs_2``: .. code-block:: idris k : Nat m : Nat -------------------------------------- - plus_commutes_rhs_2 : S (plus k m) = plus m (S k) + plus_commutes_rhs_2 : (S (plus k m)) = (plus m (S k)) It is a good idea to give these slightly more meaningful names: @@ -96,107 +94,100 @@ yields: .. code-block:: idris - plus_commutes_Z : m = plus m 0 + plus_commutes_Z : (m : Nat) -> m = plus m Z plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n - plus_commutes Z m = plus_commutes_Z + plus_commutes Z m = plus_commutes_Z m plus_commutes (S k) m = ?plus_commutes_S That is, the hole has been filled with a call to a top level -function ``plus_commutes_Z``. The argument ``m`` has been made implicit -because it can be inferred from context when it is applied. +function ``plus_commutes_Z``, applied to the variable in scope ``m``. Unfortunately, we cannot prove this lemma directly, since ``plus`` is -defined by matching on its *first* argument, and here ``plus m 0`` has a -specific value for its *second argument* (in fact, the left hand side of -the equality has been reduced from ``plus 0 m``.) Again, we can prove +defined by matching on its *first* argument, and here ``plus m Z`` has a +concrete value for its *second argument* (in fact, the left hand side of +the equality has been reduced from ``plus Z m``.) Again, we can prove this by induction, this time on ``m``. First, create a template definition with ``\d``: .. code-block:: idris - plus_commutes_Z : m = plus m 0 - plus_commutes_Z = ?plus_commutes_Z_rhs - -Since we are going to write this by induction on ``m``, which is -implicit, we will need to bring ``m`` into scope manually: - -.. code-block:: idris - - plus_commutes_Z : m = plus m 0 - plus_commutes_Z {m} = ?plus_commutes_Z_rhs + plus_commutes_Z : (m : Nat) -> m = plus m Z + plus_commutes_Z m = ?plus_commutes_Z_rhs Now, case split on ``m`` with ``\c``: .. code-block:: idris - plus_commutes_Z : m = plus m 0 - plus_commutes_Z {m = Z} = ?plus_commutes_Z_rhs_1 - plus_commutes_Z {m = (S k)} = ?plus_commutes_Z_rhs_2 + plus_commutes_Z : (m : Nat) -> m = plus m Z + plus_commutes_Z Z = ?plus_commutes_Z_rhs_1 + plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2 Checking the type of ``plus_commutes_Z_rhs_1`` shows the following, -which is easily proved by reflection: +which is provable by ``Refl``: .. code-block:: idris -------------------------------------- - plus_commutes_Z_rhs_1 : 0 = 0 + plus_commutes_Z_rhs_1 : Z = Z -For such trivial proofs, we can let write the proof automatically by -pressing ``\o`` with the cursor over ``plus_commutes_Z_rhs_1``. +For such immediate proofs, we can let write the proof automatically by +pressing ``\s`` with the cursor over ``plus_commutes_Z_rhs_1``. This yields: .. code-block:: idris - plus_commutes_Z : m = plus m 0 - plus_commutes_Z {m = Z} = Refl - plus_commutes_Z {m = (S k)} = ?plus_commutes_Z_rhs_2 + plus_commutes_Z : (m : Nat) -> m = plus m Z + plus_commutes_Z Z = Refl + plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2 For ``plus_commutes_Z_rhs_2``, we are not so lucky: .. code-block:: idris - k : Nat - -------------------------------------- - plus_commutes_Z_rhs_2 : S k = S (plus k 0) + k : Nat + ------------------------------------- + plus_commutes_Z_rhs_2 : S k = S (plus k Z) -Inductively, we should know that ``k = plus k 0``, and we can get access +Inductively, we should know that ``k = plus k Z``, and we can get access to this inductive hypothesis by making a recursive call on k, as follows: .. code-block:: idris - plus_commutes_Z : m = plus m 0 - plus_commutes_Z {m = Z} = Refl - plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in - ?plus_commutes_Z_rhs_2 + plus_commutes_Z : (m : Nat) -> m = plus m Z + plus_commutes_Z Z = Refl + plus_commutes_Z (S k) + = let rec = plus_commutes_Z k in + ?plus_commutes_Z_rhs_2 For ``plus_commutes_Z_rhs_2``, we now see: .. code-block:: idris - k : Nat - rec : k = plus k (fromInteger 0) - -------------------------------------- - plus_commutes_Z_rhs_2 : S k = S (plus k 0) + k : Nat + rec : k = plus k Z + ------------------------------------- + plus_commutes_Z_rhs_2 : S k = S (plus k Z) -Again, the ``fromInteger 0`` is merely due to ``Nat`` having an implementation -of the ``Num`` interface. So we know that ``k = plus k 0``, but how do -we use this to update the goal to ``S k = S k``? +So we know that ``k = plus k Z``, but how do we use this to update the goal to +``S k = S k``? To achieve this, Idris provides a ``replace`` function as part of the prelude: .. code-block:: idris - *pluscomm> :t replace - replace : (x = y) -> P x -> P y + Main> :t replace + Builtin.replace : (0 rule : x = y) -> p x -> p y -Given a proof that ``x = y``, and a property ``P`` which holds for +Given a proof that ``x = y``, and a property ``p`` which holds for ``x``, we can get a proof of the same property for ``y``, because we -know ``x`` and ``y`` must be the same. In practice, this function can be -a little tricky to use because in general the implicit argument ``P`` +know ``x`` and ``y`` must be the same. Note the multiplicity on ``rule`` +means that it's guaranteed to be erased at run time. +In practice, this function can be +a little tricky to use because in general the implicit argument ``p`` can be hard to infer by unification, so Idris provides a high level syntax which calculates the property and applies ``replace``: @@ -205,63 +196,48 @@ syntax which calculates the property and applies ``replace``: rewrite prf in expr If we have ``prf : x = y``, and the required type for ``expr`` is some -property of ``x``, the ``rewrite ... in`` syntax will search for ``x`` -in the required type of ``expr`` and replace it with ``y``. Concretely, -in our example, we can say: +property of ``x``, the ``rewrite ... in`` syntax will search for all +occurrences of ``x`` +in the required type of ``expr`` and replace them with ``y``. We want +to replace ``plus k Z`` with ``k``, so we need to apply our rule +``rec`` in reverse, which we can do using ``sym`` from the Prelude .. code-block:: idris - plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in - rewrite rec in ?plus_commutes_Z_rhs_2 + Main> :t sym + Builtin.sym : (0 rule : x = y) -> y = x + +Concretely, in our example, we can say: + +.. code-block:: idris + + plus_commutes_Z (S k) + = let rec = plus_commutes_Z k in + rewrite sym rec in ?plus_commutes_Z_rhs_2 Checking the type of ``plus_commutes_Z_rhs_2`` now gives: .. code-block:: idris - k : Nat - rec : k = plus k (fromInteger 0) - _rewrite_rule : plus k 0 = k - -------------------------------------- - plus_commutes_Z_rhs_2 : S (plus k 0) = S (plus k 0) - -Using the rewrite rule ``rec`` (which we can see in the context here as -``_rewrite_rule``\ [1]_, the goal type has been updated with ``k`` -replaced by ``plus k 0``. - -Alternatively, we could have applied the rewrite in the other direction -using the ``sym`` function: - -.. code-block:: idris - - *pluscomm> :t sym - sym : (l = r) -> r = l - -.. code-block:: idris - - plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in - rewrite sym rec in ?plus_commutes_Z_rhs_2 - -In this case, inspecting the type of the hole gives: - -.. code-block:: idris - - k : Nat - rec : k = plus k (fromInteger 0) - _rewrite_rule : k = plus k 0 - -------------------------------------- + k : Nat + rec : k = plus k Z + ------------------------------------- plus_commutes_Z_rhs_2 : S k = S k -Either way, we can use proof search (``\o``) to complete the -proof, giving: +Using the rewrite rule ``rec``, the goal type has been updated with ``plus k Z`` +replaced by ``k``. + +We can use proof search (``\s``) to complete the proof, giving: .. code-block:: idris - plus_commutes_Z : m = plus m 0 - plus_commutes_Z {m = Z} = Refl - plus_commutes_Z {m = (S k)} = let rec = plus_commutes_Z {m=k} in - rewrite rec in Refl + plus_commutes_Z : (m : Nat) -> m = plus m Z + plus_commutes_Z Z = Refl + plus_commutes_Z (S k) + = let rec = plus_commutes_Z k in + rewrite sym rec in Refl -The base case is now complete. +The base case of ``plus_commutes`` is now complete. Inductive Step ============== @@ -272,16 +248,16 @@ state: .. code-block:: idris plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n - plus_commutes Z m = plus_commutes_Z + plus_commutes Z m = plus_commutes_Z m plus_commutes (S k) m = ?plus_commutes_S Looking again at the type of ``plus_commutes_S``, we have: .. code-block:: idris - k : Nat - m : Nat - -------------------------------------- + k : Nat + m : Nat + ------------------------------------- plus_commutes_S : S (plus k m) = plus m (S k) Conveniently, by induction we can immediately tell that @@ -299,10 +275,9 @@ Checking the type of ``plus_commutes_S`` now gives: .. code-block:: idris - k : Nat - m : Nat - _rewrite_rule : plus m k = plus k m - -------------------------------------- + k : Nat + m : Nat + ------------------------------------- plus_commutes_S : S (plus m k) = plus m (S k) The good news is that ``m`` and ``k`` now appear in the correct order. @@ -315,17 +290,16 @@ begin by making a new top level lemma with ``\l``. This gives: plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k) -Unlike the previous case, ``k`` and ``m`` are not made implicit because -we cannot in general infer arguments to a function from its result. -Again, we make a template definition with ``\d``: +Again, we make a template definition with ``\a``: .. code-block:: idris plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k) plus_commutes_S k m = ?plus_commutes_S_rhs -Again, this is defined by induction over ``m``, since ``plus`` is -defined by matching on its first argument. The complete definition is: +Like ``plus_commutes_Z``, we can define this by induction over ``m``, since +``plus`` is defined by matching on its first argument. The complete definition +is: .. code-block:: idris @@ -344,8 +318,3 @@ which it happens to be well-defined. Now that ``plus_commutes`` has a ``total`` annotation, we have completed the proof of commutativity of addition on natural numbers. - -.. [1] - Note that the left and right hand sides of the equality have been - swapped, because ``replace`` takes a proof of ``x=y`` and the - property for ``x``, not ``y``. diff --git a/docs/proofs/pluscomm.rst b/docs/proofs/pluscomm.rst index 4622416..57a71e0 100644 --- a/docs/proofs/pluscomm.rst +++ b/docs/proofs/pluscomm.rst @@ -20,11 +20,11 @@ the prompt, the read-eval-print loop): .. code-block:: idris - Idris> \m => plus Z m - \m => m : Nat -> Nat + Main> \m => plus Z m + \m => m Idris> \k,m => plus (S k) m - \k => \m => S (plus k m) : Nat -> Nat -> Nat + \k => \m => S (plus k m) Note that unlike many other language REPLs, the Idris REPL performs evaluation on *open* terms, meaning that it can reduce terms which @@ -47,17 +47,14 @@ we must *prove* them. Equality Proofs =============== -Idris has a built-in propositional equality type, conceptually defined -as follows: +Idris defines a propositional equality type as follows: .. code-block:: idris - data (=) : a -> b -> Type where - Refl : x = x + data Equal : a -> b -> Type where + Refl : Equal x x -Note that this must be built-in, rather than defined in the library, -because ``=`` is a reserved operator — you cannot define this directly -in your own code. +As syntactic sugar, ``Equal x y`` can be written as ``x = y``. It is *propositional* equality, where the type states that any two values in different types ``a`` and ``b`` may be proposed to be equal. @@ -87,11 +84,11 @@ error: :: - When elaborating right hand side of four_eq_five: - Type mismatch between - x = x (Type of Refl) + When unifying 4 = 4 and (fromInteger 4) = (fromInteger 5) + Mismatch between: + 4 and - 4 = 5 (Expected type) + 5 Type checking equality proofs ----------------------------- @@ -131,13 +128,12 @@ equalities between values in different types: .. code-block:: idris - idris_not_php : 2 = "2" + idris_not_php : Z = "Z" -Obviously, in Idris the type ``2 = "2"`` is uninhabited, and one might -wonder why it is useful to be able to propose equalities between values -in different types. However, with dependent types, such equalities can -arise naturally. For example, if two vectors are equal, their lengths -must be equal: +The type ``Z = "Z"`` is uninhabited, and one might wonder why it is useful to +be able to propose equalities between values in different types. However, with +dependent types, such equalities can arise naturally. For example, if two +vectors are equal, their lengths must be equal: .. code-block:: idris diff --git a/docs/proofs/propositional.rst b/docs/proofs/propositional.rst index 92ccbc0..0159b24 100644 --- a/docs/proofs/propositional.rst +++ b/docs/proofs/propositional.rst @@ -1,59 +1,68 @@ -This page attempts to explain some of the techniques used in Idris to prove propositional equalities. +This page attempts to explain some of the techniques used in Idris to prove +propositional equalities. Proving Propositional Equality ============================== -We have seen that definitional equalities can be proved using Refl since they always normalise to unique values that can be compared directly. +We have seen that definitional equalities can be proved using ``Refl`` since they +always normalise to values that can be compared directly. -However with propositional equalities we are using symbolic variables they do not always normalse. +However with propositional equalities we are using symbolic variables, which do +not always normalse. So to take the previous example: -plusReducesR : (n:Nat) -> plus n Z = n +.. code-block:: idris -In this case 'plus n Z' does not normalise to n. Even though both sides are equal we cannot pattern match Refl. + plusReducesR : (n : Nat) -> plus n Z = n -If the pattern match cannot match for all 'n' then the way around this is to separately match all possible values of 'n'. In the case of natural numbers we do this by induction. +In this case ``plus n Z`` does not normalise to n. Even though both sides of +the equality are provably equal we cannot claim ``Refl`` as a proof. -So here: +If the pattern match cannot match for all ``n`` then we need to +match all possible values of ``n``. In this case .. code-block:: idris - plusReducesR : n = plus n 0 - plusReducesR {n = Z} = Refl - plusReducesR {n = (S k)} = let rec = plus_commutes_Z {n=k} in - rewrite rec in Refl + plusReducesR : (n : Nat) -> plus n Z = n + plusReducesR Z = Refl + plusReducesR (S k) + = let rec = plusReducesR k in + rewrite sym rec in Refl -we don't call Refl to match on 'n = plus n 0' forall 'n' we call it for every number separately. So, in the second line, the pattern matcher knows to substitute Z for n in the type being matched. This uses 'rewrite' which is explained below. +we can't use ``Refl`` to prove ``n = plus n 0`` for all ``n``. Instead, we call +it for each case separately. So, in the second line for example, the type checker +substitutes ``Z`` for ``n`` in the type being matched, and reduces the type +accordingly. Replace ======= -This implements the 'indiscernability of identicals' principle, if two terms are equal then they have the same properties. In other words, if x=y, then we can substitute y for x in any expression. In our proofs we can express this as: +This implements the 'indiscernability of identicals' principle, if two terms +are equal then they have the same properties. In other words, if ``x=y``, then we +can substitute y for x in any expression. In our proofs we can express this as: if x=y - then P x = P y + then prop x = prop y -where P is a pure function representing the property. In the examples below P is an expression in some variable with a type like this: P: n -> Type +where prop is a pure function representing the property. In the examples below +prop is an expression in some variable with a type like this: ``prop: n -> Type`` -So if n is a natural number variable then P could be something like 2*n + 3. +So if ``n`` is a natural number variable then ``prop`` could be something +like ``\n => 2*n + 3``. To use this in our proofs there is the following function in the prelude: .. code-block:: idris ||| Perform substitution in a term according to some equality. - replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y + replace : forall x, y, prop . (0 rule : x = y) -> prop x -> prop y replace Refl prf = prf -Removing the implicits, if we supply an equality (x=y) and a proof of a property of x (P x) then we get a proof of a property of y (P y) - -.. code-block:: idris - - > :t replace - replace : (x = y) -> P x -> P y - -So, in the following example, if we supply p1 x which is a proof that x=2 and the equality x=y then we get a proof that y=2. +If we supply an equality (x=y) and a proof of a property of x (``prop x``) then we get +a proof of a property of y (``prop y``). +So, in the following example, if we supply ``p1 x`` which is a proof that ``x=2`` and +the equality ``x=y`` then we get a proof that ``y=2``. .. code-block:: idris @@ -66,16 +75,13 @@ So, in the following example, if we supply p1 x which is a proof that x=2 and th Rewrite ======= -Similar to 'replace' above but Idris provides a nicer syntax which makes 'rewrite' easier to use in examples like plusReducesR above. +In practice, ``replace`` can be +a little tricky to use because in general the implicit argument ``prop`` +can be hard to infer for the machine, so Idris provides a high level +syntax which calculates the property and applies ``replace``. -.. code-block:: idris - - rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x - rewrite__impl p Refl prf = prf - -The difference from 'replace' above is nicer syntax and the property p1 is explicitly supplied and it goes in the opposite direction (input and output reversed). - -Example: again we supply p1 which is a proof that x=2 and the equality x=y then we get a proof that y=2. +Example: again we supply ``p1`` which is a proof that ``x=2`` and the equality +``x=y`` then we get a proof that ``y=2``. .. code-block:: idris @@ -85,27 +91,28 @@ Example: again we supply p1 which is a proof that x=2 and the equality x=y then testRewrite2: (x=y) -> (p1 y) -> (p1 x) testRewrite2 a b = rewrite a in b -We can think of rewrite doing this: +We can think of ``rewrite`` as working in this way: - * Start with a equation x=y and a property P: x -> Type - * Searches y in P - * Replaces all occurrences of y with x in P. + * Start with a equation ``x=y`` and a property ``prop : x -> Type`` + * Search for ``x`` in ``prop`` + * Replaces all occurrences of ``x`` with ``y`` in ``prop``. That is, we are doing a substitution. Symmetry and Transitivity ========================= -In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' and these are also included in the prelude: +In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity' +and these are also included in the prelude: .. code-block:: idris ||| Symmetry of propositional equality - sym : {left:a} -> {right:b} -> left = right -> right = left + sym : forall x, y . (0 rule : x = y) -> y = x sym Refl = Refl ||| Transitivity of propositional equality - trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c + trans : forall a, b, c . (0 l : a = b) -> (0 r : b = c) -> a = c trans Refl Refl = Refl Heterogeneous Equality diff --git a/samples/Proofs.idr b/samples/Proofs.idr index 7109d53..c5fa68d 100644 --- a/samples/Proofs.idr +++ b/samples/Proofs.idr @@ -17,6 +17,9 @@ disjoint n prf = replace {p = disjointTy} prf () plusReduces : (n:Nat) -> plus Z n = n plusReduces n = Refl +plusReducesR : (n:Nat) -> plus n Z = n +plusReducesR n = Refl + plusReducesZ : (n:Nat) -> n = plus n Z plusReducesZ Z = Refl plusReducesZ (S k) = cong S (plusReducesZ k) diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 9a5fbe9..90cc66b 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -312,7 +312,7 @@ addMadeLemma n ty app line content where -- Put n : ty in the first blank line insertInBlank : List String -> List String - insertInBlank [] = [show n ++ " : " ++ ty ++ "\n\n"] + insertInBlank [] = [show n ++ " : " ++ ty ++ "\n"] insertInBlank (x :: xs) = if trim x == "" then ("\n" ++ show n ++ " : " ++ ty ++ "\n") :: xs diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 259a2db..d2bb84a 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -102,7 +102,11 @@ sugarApp tm@(PApp fc (PApp _ (PRef _ (UN "DPair")) l) rb) sugarApp (PApp fc (PApp _ (PRef _ (UN "MkDPair")) l) r) = PDPair fc (unbracket l) (PImplicit fc) (unbracket r) sugarApp (PApp fc (PApp _ (PRef _ (UN "Equal")) l) r) - = PEq fc l r + = PEq fc (unbracket l) (unbracket r) +sugarApp (PApp fc (PApp _ (PRef _ (UN "===")) l) r) + = PEq fc (unbracket l) (unbracket r) +sugarApp (PApp fc (PApp _ (PRef _ (UN "~=~")) l) r) + = PEq fc (unbracket l) (unbracket r) sugarApp (PRef fc (UN "Nil")) = PList fc [] sugarApp (PRef fc (UN "Unit")) = PUnit fc sugarApp (PRef fc (UN "MkUnit")) = PUnit fc diff --git a/src/TTImp/Interactive/MakeLemma.idr b/src/TTImp/Interactive/MakeLemma.idr index e426c66..654ec56 100644 --- a/src/TTImp/Interactive/MakeLemma.idr +++ b/src/TTImp/Interactive/MakeLemma.idr @@ -41,8 +41,8 @@ getArgs : {auto c : Ref Ctxt Defs} -> Env Term vars -> Nat -> Term vars -> Core (List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp), RawImp) getArgs {vars} env (S k) (Bind _ x (Pi c p ty) sc) - = do ty' <- unelab env ty - defs <- get Ctxt + = do defs <- get Ctxt + ty' <- unelab env !(normalise defs env ty) let x' = UN !(uniqueName defs (map nameRoot vars) (nameRoot x)) (sc', ty) <- getArgs (Pi c p ty :: env) k (renameTop x' sc) -- Don't need to use the name if it's not used in the scope type @@ -56,7 +56,8 @@ getArgs {vars} env (S k) (Bind _ x (Pi c p ty) sc) else Implicit pure ((x, mn, p', c, ty') :: sc', ty) getArgs env k ty - = do ty' <- unelab env ty + = do defs <- get Ctxt + ty' <- unelab env !(normalise defs env ty) pure ([], ty') mkType : FC -> List (Name, Maybe Name, PiInfo RawImp, RigCount, RawImp) -> diff --git a/tests/idris2/basic014/expected b/tests/idris2/basic014/expected index 89bf1da..495a98e 100644 --- a/tests/idris2/basic014/expected +++ b/tests/idris2/basic014/expected @@ -1,5 +1,5 @@ 1/1: Building Rewrite (Rewrite.idr) Rewrite.idr:15:25--17:1:While processing right hand side of Main.wrongCommutes at Rewrite.idr:15:1--17:1: -Rewriting by (m + k) = (k + m) did not change type (S k + m) = (m + S k) +Rewriting by m + k = k + m did not change type S k + m = m + S k Rewrite.idr:19:26--20:1:While processing right hand side of Main.wrongCommutes2 at Rewrite.idr:19:1--20:1: Nat is not a rewrite rule type diff --git a/tests/idris2/basic016/expected b/tests/idris2/basic016/expected index 4bccce2..8326240 100644 --- a/tests/idris2/basic016/expected +++ b/tests/idris2/basic016/expected @@ -1,19 +1,19 @@ 1/1: Building Eta (Eta.idr) Eta.idr:14:10--15:1:While processing right hand side of Main.etaBad at Eta.idr:14:1--15:1: -When unifying ?x = ?x and MkTest = (\x => (\y => (MkTest ?_ ?_))) +When unifying ?x = ?x and MkTest = \x => (\y => (MkTest ?_ ?_)) Mismatch between: Integer and Nat 1/1: Building Eta2 (Eta2.idr) Eta2.idr:2:8--4:1:While processing right hand side of Main.test at Eta2.idr:2:1--4:1: -When unifying ?x = ?x and S = (\x => (S ?_)) +When unifying ?x = ?x and S = \x => (S ?_) Mismatch between: Nat and a Eta2.idr:5:44--6:1:While processing right hand side of Main.test2 at Eta2.idr:5:1--6:1: -When unifying ?x = ?x and S = (\x => (S ?_)) +When unifying ?x = ?x and S = \x => (S ?_) Mismatch between: Nat and diff --git a/tests/idris2/interactive012/expected b/tests/idris2/interactive012/expected index 25dd189..75fc98c 100644 --- a/tests/idris2/interactive012/expected +++ b/tests/idris2/interactive012/expected @@ -1,7 +1,7 @@ 1/1: Building WithLift (WithLift.idr) -Main> succNotZero : (S k) = Z -> Void +Main> succNotZero : S k = Z -> Void succNotZero -Main> recNotEqLift : (k = j -> Void) -> (S k) = (S j) -> Void +Main> recNotEqLift : (k = j -> Void) -> S k = S j -> Void (recNotEqLift contra) Main> recNotEq f Refl = f Refl Main> Bye for now!