Instantly share code, notes, and snippets.

Embed
What would you like to do?
Z + n = n, (S n) + m = S (n + m)
%default total
record PlusLike : (Nat -> Nat -> Nat) -> Type where
PL : {plus : Nat -> Nat -> Nat} ->
(plusIdentity : (n : Nat) -> plus Z n = n) ->
(plusSucc : (n, m : Nat) -> plus (S n) m = S (plus n m)) ->
PlusLike plus
isPlus : (f : Nat -> Nat -> Nat) -> PlusLike f -> (n, m : Nat) -> f n m = plus n m
isPlus f (PL plusIdentity _) Z m = plusIdentity m
isPlus f (PL plusIdentity plusSucc) (S k) m =
let inductiveHypothesis = isPlus f (PL plusIdentity plusSucc) k m
in ?isPlusStepCase
---------- Proofs ----------
isPlusStepCase = proof
intros
rewrite sym (plusSucc k m)
rewrite inductiveHypothesis
trivial
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment