help with subtypes and functions

Stream: new members

[Colin Jones ⚛️]

How do I get Lean to realize that the valid requirement in dna_to_rna_forward is proven by a hypothesis in dna_to_rna which uses dna_to_rna_forward?

open Function Classical

/- # Definition of Nucleotide Base #
  U := Uracil
  A := Adenosine
  G := Guanosine
  C := Cytosine
  T := Thymine
  I := Inosine
  N := Anything else
-/
inductive NucBase
  | U | A | G | C | T | I | N
open NucBase
deriving instance Repr for NucBase


/- # General Definitions # -/
def NucBase.isRNABase (b : NucBase) : Bool := b matches U | A | G | C | I

def NucBase.isDNABase (b : NucBase) : Bool := b matches T | A | G | C

def redundant (f : α → β) : Prop := ¬ Injective f


/- # DNA Function Definitions # -/
def dna_to_rna_singlet (n : NucBase) (valid : n.isDNABase = True) :=
  match n with
  | T => A
  | A => U
  | G => C
  | C => G

def dna_to_rna_forward (s : List NucBase) (valid : ∀ n ∈ s, n.isDNABase = True):=
  s.map dna_to_rna_singlet -- Error here with types

[Eric Paul]

Here's a working fix, although I haven't used attach much so there might be a better way.
In essence, writing s.attach.map means that the function in the map is given a term of type {x // x ∈ s}. So we have access to the fact that this term is an element of s, which we need to use valid.

import Mathlib

open Function

/- # Definition of Nucleotide Base #
  U := Uracil
  A := Adenosine
  G := Guanosine
  C := Cytosine
  T := Thymine
  I := Inosine
  N := Anything else
-/
inductive NucBase
  | U | A | G | C | T | I | N
open NucBase
deriving instance Repr for NucBase


/- # General Definitions # -/
def NucBase.isRNABase (b : NucBase) : Bool := b matches U | A | G | C | I

def NucBase.isDNABase (b : NucBase) : Bool := b matches T | A | G | C

def redundant (f : α → β) : Prop := ¬ Injective f


/- # DNA Function Definitions # -/
def dna_to_rna_singlet (n : NucBase) (valid : n.isDNABase) :=
  match n with
  | T => A
  | A => U
  | G => C
  | C => G

def dna_to_rna_forward (s : List NucBase) (valid : ∀ n ∈ s, n.isDNABase):=
  s.attach.map (fun (n : {x // x ∈ s}) => dna_to_rna_singlet n (valid n n.prop))

#eval dna_to_rna_forward [T, A, G] (by simp [isDNABase])

[Derek Rhodes]

This works too and doesn't have the Mathlib requirement:

def dna_to_rna_forward (s : List NucBase) (valid : ∀ n ∈ s, n.isDNABase) :=
  s.pmap dna_to_rna_singlet valid

I just stumbled onto pmap looking in the source for Init.Data.List.Attach.lean, it happened to be at the top of the file.

[Colin Jones ⚛️]

Thank you! The new revised definition with pmap is very helpful. I have another function that uses dna_to_rna_forward. Would it be possible to provide a Repr for this function?

def dna_to_rna_forward (s : List NucBase) (valid : ∀ n ∈ s, n.isDNABase = True):=
  s.pmap dna_to_rna_singlet valid

def dna_to_rna (s : List NucBase) (valid : ∀ n ∈ s, n.isDNABase = True) : List NucBase :=
  (s.reverse |> dna_to_rna_forward)
  (by intro n hn; have h : n ∈ s := List.mem_reverse.mp hn; have h1 : n.isDNABase = True :=
    valid n h; assumption)
#eval dna_to_rna [A, T, C, T] -- HERE is error

[Colin Jones ⚛️]

In other words tell lean it's okay to Eval? Would I have to implement an option to give an output even if users don't input a valid DNA Base like Uracil (U)?

[Colin Jones ⚛️]

I found out that in Lean you have to prove that the input is valid e.g.

def dna_to_rna (s : List NucBase) (valid : ∀ n ∈ s, n.isDNABase = True) : List NucBase :=
  (s.reverse |> dna_to_rna_forward)
  (by intro n hn; have h : n ∈ s := List.mem_reverse.mp hn; have h1 : n.isDNABase = True :=
    valid n h; assumption)
#eval dna_to_rna [A, T, C, T] (by intro n hn; sorry)

[Colin Jones ⚛️]

Nevermind, I figured it out. Thank you both for the help!

def dna_to_rna (s : List NucBase) (valid : ∀ n ∈ s, n.isDNABase = True) : List NucBase :=
  (s.reverse |> dna_to_rna_forward)
  (by intro n hn; have h : n ∈ s := List.mem_reverse.mp hn; have h1 : n.isDNABase = True :=
    valid n h; assumption)
#eval dna_to_rna [A, T, C, T] (by intro n hn; aesop) -- aesop clears the goal

[Colin Jones ⚛️]

Would this be possible to prove for only n.isDNABase = True?

def dna_to_rna_singlet (n : NucBase) (valid : n.isDNABase = True) :=
  match n with
  | T => A
  | A => U
  | G => C
  | C => G

theorem injective_dna_to_rna_singlet : Injective dna_to_rna_singlet := by
  simp only [Injective]
  sorry

[Derek Rhodes]

I think Injective only works with functions of arity one, so I added a hypothesis (n : NucBase) to the new theorem, (could have used a forall), maybe this is not what you're after,

import Mathlib
open Function Classical

/- # Definition of Nucleotide Base #
  U := Uracil
  A := Adenosine
  G := Guanosine
  C := Cytosine
  T := Thymine
  I := Inosine
  N := Anything else
-/
inductive NucBase
  | U | A | G | C | T | I | N
open NucBase
deriving instance Repr for NucBase


/- # General Definitions # -/
def NucBase.isRNABase (b : NucBase) : Bool := b matches U | A | G | C | I

def NucBase.isDNABase (b : NucBase) : Bool := b matches T | A | G | C
--def redundant (f : α → β) : Prop := ¬ Injective f


/- # DNA Function Definitions # -/
def dna_to_rna_singlet (n : NucBase) (valid : n.isDNABase = True) :=
  match n with
  | T => A
  | A => U
  | G => C
  | C => G


def dna_to_rna_forward (s : List NucBase) (valid : ∀ n ∈ s, n.isDNABase) :=
  s.pmap dna_to_rna_singlet valid

theorem injective_dna_to_rna_singlet (n : NucBase) : Injective (dna_to_rna_singlet n) := by
  intro x₁ x₂ hx
  rfl

(also had to import Mathlib)

[Colin Jones ⚛️]

Yeah I tried dding the n : NucBase, but that just makes a trivial proof. I'm wondering how to transform the (n : NucBase) → n.isDNABase = decide True → NucBase : Type into (n : NucBase) → NucBase : Type if possible

[Colin Jones ⚛️]

In other words I want to prove that dna_to_rna_singlet is injective for the inputs that are allowed.

[Aaron Liu]

You can use docs#Subtype to uncurry the proof obligation.

[Colin Jones ⚛️]

Could you give more specific help? I've looked at the docs, but I still can't figure out a way to remove the middle implication

[Yakov Pechersky]

I don't think the Injective of the valid prop is what you're looking for, which is what Injective (dna_to_rna_singlet n) is discussing. One sec.

[Yakov Pechersky]

Here is the injectivity of the function:

theorem injective_dna_to_rna_singlet :
    Injective (fun n : {x // NucBase.isDNABase x} ↦ dna_to_rna_singlet n n.prop) := by
  rintro ⟨n, hn⟩ ⟨m, hm⟩
  cases n <;> cases m <;>
  any_goals simp [isDNABase] at hn hm -- remove contradictions
  all_goals simp [dna_to_rna_singlet] -- now, only DNA bases left, unfold the function

[Yakov Pechersky]

"For all nucleobases such that they are DNA bases, the function sending it to an RNA single base (which by the way requires not just the base as input but also its DNABase-ness) is injective"

[Yakov Pechersky]

Here is a similar function that uses junk values, but the theorem remains true.

def dna_to_rna_singlet_with_junk (n : NucBase) :=
  match n with
  | T => A
  | A => U
  | G => C
  | C => G
  | _ => N

theorem injOn_dna_to_rna_singlet_with_junk :
     {x | NucBase.isDNABase x}.InjOn dna_to_rna_singlet_with_junk := by
  intro n hn m hm
  cases n <;> cases m <;>
  any_goals simp [isDNABase] at hn hm -- remove contradictions
  all_goals simp [dna_to_rna_singlet_with_junk] -- now, only DNA bases left, unfold the function

theorem injective_dna_to_rna_singlet_with_junk :
    Injective (fun n : {x // NucBase.isDNABase x} ↦ dna_to_rna_singlet_with_junk n) :=
  injOn_dna_to_rna_singlet_with_junk.injective

[Colin Jones ⚛️]

Thank you a lot! The abstraction of the function out was a clever trick. I appreciate all the help

[Colin Jones ⚛️]

set_option diagnostics true
theorem redundant_genetic_code :
    redundant (fun s : {x : List NucBase // ∀ n ∈ x, n.isDNABase = True} ↦ dna_to_amino s s.prop)
    := by
  simp only [redundant, Injective, not_forall]
  use [A,A,A]

Is there a way I can show that [A,A,A] is of type { x // ∀ n ∈ x, n.isDNABase = decide True }. Here is the full file for anyone to see since there's already a lot of code above.
GeneticCode - Copy.lean

[Aaron Liu]

Instead of writing ∀ n ∈ x, n.isDNABase = True, you should just write ∀ n ∈ x, n.isDNABase.

[Colin Jones ⚛️]

Thank you, I simplified

[Aaron Liu]

You can do use ⟨[A, A, A], by decide⟩

[Colin Jones ⚛️]

Ohh that's the syntax! Okay appreciate it, I was trying to use parentheses