mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
Merge branch 'master' into AirShooter_animation
This commit is contained in:
commit
f948665b0d
@ -303,9 +303,9 @@ In order to run this or any other app you should follow this steps:
|
||||
- The app should be in `base/App` folder
|
||||
- Install necessary packages in web folder with `npm i --prefix web/`
|
||||
- Install `js-beautify` using `sudo npm i -g js-beautify`
|
||||
- Run our local server with `node web/server`
|
||||
- Build the app you want with `node web/build App.[name of app]` (in this example would be `node web/build App.Hello`)
|
||||
- Open `localhost` in your favorite browser and see your app working
|
||||
- Build the app you want with `node web/build [name of app]` (in this example would be `node web/build Hello`)
|
||||
- Run a local server with `node web/server.js 8080`
|
||||
- Open http://localhost:8080 in your favorite browser and see your app working
|
||||
|
||||
|
||||
Future work
|
||||
|
269
base/App/Checkers.kind
Normal file
269
base/App/Checkers.kind
Normal file
@ -0,0 +1,269 @@
|
||||
App.Checkers.State: App.State
|
||||
App.State.new(App.Checkers.Local, App.Checkers.Board)
|
||||
|
||||
type App.Checkers.Local {
|
||||
new(
|
||||
mouse_pos: Pair<U32, U32>
|
||||
selected: Maybe<Pair<Nat, Nat>>
|
||||
team: Bits
|
||||
)
|
||||
}
|
||||
|
||||
App.Checkers.room: String
|
||||
"test_room_02"
|
||||
|
||||
App.Checkers.scale: U32
|
||||
2
|
||||
|
||||
App.Checkers.Board: Type
|
||||
Pair<Bits, Bits>
|
||||
|
||||
|
||||
App.Checkers.tile_size: U32
|
||||
32#32
|
||||
|
||||
// Initial state
|
||||
App.Checkers.init: App.Init<App.Checkers.State>
|
||||
let mouse_pos = {0#32 0#32}
|
||||
let selected = none
|
||||
let team = Bits.o(Bits.e)
|
||||
let chunk0 = Bits.trim(60, Nat.to_bits(9817068105)) // 000000000000000000000000001001001001001001001001001001001001
|
||||
let chunk1 = Bits.trim(60, Nat.to_bits(29451204315)) // 000000000000000000000000011011011011011011011011011011011011
|
||||
let local = App.Checkers.Local.new(mouse_pos, selected, team)
|
||||
let board = {chunk0, chunk1}
|
||||
App.Store.new<App.Checkers.State>(local, board)
|
||||
|
||||
App.Checkers.get(x: Nat, y: Nat, board: App.Checkers.Board): Bits
|
||||
let tile_size = 3 :: Nat
|
||||
// X is divided by 2 because the bitcode does not contain all tiles
|
||||
// It only contains black tiles
|
||||
let index = ((x / 2) * tile_size) + (y * tile_size * 4)
|
||||
let chunk = if index <? 60 then board@fst else board@snd
|
||||
let tile = Bits.slice(3, Bits.drop(index % 60, chunk))
|
||||
tile
|
||||
|
||||
App.Checkers.canvas(local: App.Checkers.Local, board: App.Checkers.Board, img: VoxBox): VoxBox
|
||||
let size = App.Checkers.tile_size
|
||||
for i from 0 to 64 with img:
|
||||
let x = i % 8
|
||||
let y = i / 8
|
||||
// We have to draw all the 64 tiles in the board
|
||||
// However, we only store half of the board in the bitcode.
|
||||
// For this reason, we should only access the bits on even tiles
|
||||
// "is_tile" returns true if we're accessing a tile presente in the bitcode
|
||||
let is_tile = Nat.odd(x + y)
|
||||
let draw = VoxBox.Draw.image(((Nat.to_u32(x) * size) - 128) + size/ 2, ((Nat.to_u32(y) * size) - 128) + size/2)
|
||||
// Draws corresponding tile
|
||||
let img = if not(is_tile) then draw(0, App.Checkers.White_Tile, img) else draw(0, App.Checkers.Black_Tile, img)
|
||||
if is_tile then
|
||||
let tile = App.Checkers.get(x, y, board)
|
||||
// Checks if there is a piece on that tile
|
||||
if Bits.slice(1, tile) =? Bits.o(Bits.e) then
|
||||
img
|
||||
else
|
||||
// Draws the piece corresponding to the bits in the tile
|
||||
switch Bits.eql(Bits.drop(1, tile)) {
|
||||
Bits.o(Bits.o(Bits.e)): draw(2, App.Checkers.Black_Normal, img)
|
||||
Bits.i(Bits.o(Bits.e)): draw(2, App.Checkers.Red_Normal, img)
|
||||
Bits.o(Bits.i(Bits.e)): draw(2, App.Checkers.Black_Queen, img)
|
||||
Bits.i(Bits.i(Bits.e)): draw(2, App.Checkers.Red_Queen, img)
|
||||
}default img
|
||||
else
|
||||
img
|
||||
let selected = local@selected
|
||||
without selected: img
|
||||
let {x, y} = {Nat.to_u32(selected@fst), Nat.to_u32(selected@snd)}
|
||||
// Draws the outline if there is one
|
||||
VoxBox.Draw.image(((x * size) - 128) + size/2, ((y * size) - 128) + size/2, 1, App.Checkers.Outline, img)
|
||||
|
||||
// Render function
|
||||
App.Checkers.draw(img: VoxBox): App.Draw<App.Checkers.State>
|
||||
(state)
|
||||
let local = state@local
|
||||
let global = state@global
|
||||
// Updates canvas
|
||||
let new_img = App.Checkers.canvas(local, global, img)
|
||||
<div>
|
||||
{
|
||||
DOM.vbox(
|
||||
{
|
||||
"id": "game_screen",
|
||||
"width": "256"
|
||||
"height": "256"
|
||||
"scale": U32.show(App.Checkers.scale)
|
||||
}, {}, new_img)
|
||||
}
|
||||
</div>
|
||||
|
||||
App.Checkers.is_move_possible(x0: Nat, y0: Nat, x1: Nat, y1: Nat, team: Bits, board: App.Checkers.Board): Bool
|
||||
let one = Bits.i(Bits.e) // 1
|
||||
let zero = Bits.o(Bits.e) // 0
|
||||
// Origin tile
|
||||
let from_tile = App.Checkers.get(x0, y0, board)
|
||||
// Destination tile
|
||||
let to_tile = App.Checkers.get(x1, y1, board)
|
||||
// Checks if piece exists
|
||||
let piece_exists = Bits.eql(Bits.slice(1, from_tile), one)
|
||||
// Checks if you own the origin unit
|
||||
let piece_owner = Bits.eql(Bits.slice(1, Bits.drop(1, from_tile)), team)
|
||||
// Checks if destination is empty
|
||||
let to_is_empty = Bits.eql(Bits.slice(1, to_tile), zero)
|
||||
// Counts how many tiles you moved forward
|
||||
let move_forward = if Bits.i(Bits.e) =? team then y0 - y1 else y1 - y0
|
||||
// Counts how many tiles you moved sideway
|
||||
let move_sideway = if x0 >? x1 then x0 - x1 else x1 - x0
|
||||
// Checks if destination is adjacent and in front of piece
|
||||
let move_allowed = (move_forward =? 1) && (move_sideway =? 1)
|
||||
// Checks if player's team correspond to team turn
|
||||
let is_user_turn = Bits.drop(59 board@snd) =? team
|
||||
// Checks all conditions necessary to move a piece
|
||||
if piece_exists && piece_owner && to_is_empty && is_user_turn then
|
||||
// Checks if you are moving instead of jumping pieces
|
||||
if move_allowed then
|
||||
true
|
||||
else
|
||||
// Checks if you're jumping a piece
|
||||
if (move_forward =? 2) && (move_sideway =? 2) then
|
||||
// Tile to jump
|
||||
let mid_tile = App.Checkers.get(if x0 >? x1 then x1 + 1 else x0 + 1, if y0 >? y1 then y1 + 1 else y0 + 1, board)
|
||||
// Checks if there is a piece to jump
|
||||
let mid_is_full = Bool.not(Bits.eql(Bits.slice(1, mid_tile), zero))
|
||||
// Checks if the piece to jump is an enemy
|
||||
let mid_is_enemy = Bool.not(Bits.eql(Bits.slice(1, Bits.drop(1, mid_tile)), team))
|
||||
mid_is_full && piece_owner
|
||||
else
|
||||
false
|
||||
else
|
||||
false
|
||||
|
||||
|
||||
|
||||
|
||||
App.Checkers.move(code: Bits, board: App.Checkers.Board): App.Checkers.Board
|
||||
// Divides the bitcode into team and coordinates
|
||||
let team = Bits.slice(1, code)
|
||||
let x0 = Bits.slice(3, Bits.drop(1, code))
|
||||
let y0 = Bits.slice(3, Bits.drop(4, code))
|
||||
let x1 = Bits.slice(3, Bits.drop(7, code))
|
||||
let y1 = Bits.slice(3, Bits.drop(10, code))
|
||||
let is_possible = App.Checkers.is_move_possible(Bits.to_nat(x0), Bits.to_nat(y0), Bits.to_nat(x1), Bits.to_nat(y1), team, board)
|
||||
// Executes an movement if possible
|
||||
if is_possible then
|
||||
App.Checkers.move.aux(Bits.to_nat(x0), Bits.to_nat(y0), Bits.to_nat(x1), Bits.to_nat(y1), team, board)
|
||||
else
|
||||
board
|
||||
|
||||
|
||||
App.Checkers.move.aux(x0: Nat, y0: Nat, x1: Nat, y1: Nat, team: Bits, board: App.Checkers.Board): App.Checkers.Board
|
||||
// Gets how many bits we need to skip in order to reach the target bit
|
||||
let from_index = ((x0 / 2) * 3) + (y0 * 12)
|
||||
// Gets which chunk to access
|
||||
let from_chunk = if Nat.ltn(from_index, 60) then board@fst else board@snd
|
||||
// Gets the tile to move
|
||||
let from_tile = Bits.slice(3, Bits.drop(from_index % 60, from_chunk))
|
||||
// Creates an empty tile to place in from_tile's place
|
||||
let new_tile = Bits.o(Bits.o(Bits.o(Bits.e)))
|
||||
// Updates chunk
|
||||
let from_chunk = Bits.set(from_index % 60, new_tile, from_chunk)
|
||||
// Places the chunk without the piece back into the board
|
||||
let new_board = if Nat.ltn(from_index, 60) then board@fst <- from_chunk else board@snd <- from_chunk
|
||||
|
||||
// Gets how many bits we need to skip in order to reach the destination bit
|
||||
let to_index = ((x1 / 2) * 3) + (y1 * 12)
|
||||
// Gets which chunk to access
|
||||
let to_chunk = if Nat.ltn(to_index, 60) then new_board@fst else new_board@snd
|
||||
// Places the origin tile into the new position
|
||||
let to_chunk = Bits.set(to_index % 60, from_tile, to_chunk)
|
||||
// Places the chunk with the piece's new position into the board
|
||||
let new_board = if Nat.ltn(to_index, 60) then new_board@fst <- to_chunk else new_board@snd <- to_chunk
|
||||
// Changes the turn in the bitcode
|
||||
let new_board = new_board@snd <- Bits.set(59, Bits.not(team), new_board@snd)
|
||||
|
||||
let forward_2 = if Bits.i(Bits.e) =? team then (y0 - y1) =? 2 else (y1 - y0) =? 2
|
||||
let sideway_2 = if x0 >? x1 then (x0 - x1) =? 2 else (x1 - x0) =? 2
|
||||
// Checks if you are jumping a piece
|
||||
if forward_2 && sideway_2 then
|
||||
// Gets how many bits we need to skip in order to reach the mid bits
|
||||
let mid_index = (((Nat.min(x0, x1) + 1) / 2) * 3) + ((Nat.min(y0, y1) + 1) * 12)
|
||||
// Gets which chunk to access
|
||||
let mid_chunk = if Nat.ltn(mid_index, 60) then new_board@fst else new_board@snd
|
||||
// Removes the piece from the mid_chunk
|
||||
let mid_chunk = Bits.set(mid_index % 60, new_tile, mid_chunk)
|
||||
// Places the chunk without the jumped piece into the board
|
||||
let new_board = if Nat.ltn(mid_index, 60) then new_board@fst <- mid_chunk else new_board@snd <- mid_chunk
|
||||
new_board
|
||||
else
|
||||
new_board
|
||||
|
||||
// Converts the mouse coordinate into board coordinates
|
||||
App.Checkers.mouse_to_coord(mouse_pos: Pair<U32, U32>): Pair<Nat, Nat>
|
||||
let scale = App.Checkers.scale
|
||||
let tile_size = App.Checkers.tile_size
|
||||
let x = mouse_pos@fst / (scale * tile_size)
|
||||
let y = mouse_pos@snd / (scale * tile_size)
|
||||
{U32.to_nat(x), U32.to_nat(y)}
|
||||
|
||||
// Event handler
|
||||
App.Checkers.when: App.When<App.Checkers.State>
|
||||
(event, state)
|
||||
let local = state@local
|
||||
let board = state@global
|
||||
let room = String.take(16, Crypto.Keccak.hash(App.Checkers.room))
|
||||
case event {
|
||||
init: App.watch!(room)
|
||||
key_down:
|
||||
if event.code =? 'T' then App.set_local!(local@team <- Bits.not(local@team)) else App.pass!
|
||||
mouse_down:
|
||||
log("x: " | U32.show(local@mouse_pos@fst) | " y: " | U32.show(local@mouse_pos@snd))
|
||||
let selected = local@selected
|
||||
let coord = App.Checkers.mouse_to_coord(local@mouse_pos)
|
||||
case selected {
|
||||
none:
|
||||
let local = local@selected <- some(coord)
|
||||
App.set_local!(local)
|
||||
some:
|
||||
let {x0, y0} = selected.value
|
||||
let {x1, y1} = coord
|
||||
let is_possible = App.Checkers.is_move_possible(x0, y0, x1, y1, local@team, board)
|
||||
let f = (x: Nat) Bits.trim(3, Nat.to_bits(x))
|
||||
log("when x0: " | Bits.show(f(x0)) | " y0: " | Bits.show(f(y0)) | " x1: " | Bits.show(f(x1)) | " y1: " | Bits.show(f(y1)))
|
||||
if is_possible then
|
||||
let code = Bits.concat(local@team, Bits.concat(f(x0), Bits.concat(f(y0), Bits.concat(f(x1), f(y1)))))
|
||||
log(Bits.show(code))
|
||||
let code = Bits.show(code)
|
||||
IO {
|
||||
App.new_post!(room, code)
|
||||
App.set_local!(local@selected <- none)
|
||||
}
|
||||
else
|
||||
App.set_local!(local@selected <- none)
|
||||
}
|
||||
mouse_move:
|
||||
let local = local@mouse_pos <- event.mouse_pos
|
||||
App.set_local!(local)
|
||||
} default App.pass!
|
||||
|
||||
// Global ticker
|
||||
App.Checkers.tick: App.Tick<App.Checkers.State>
|
||||
App.no_tick<App.Checkers.State>
|
||||
|
||||
// Global visitor
|
||||
App.Checkers.post: App.Post<App.Checkers.State>
|
||||
(time, room, addr, data, glob)
|
||||
let code = Bits.read(data)
|
||||
case code {
|
||||
o: App.Checkers.move(code.pred, glob)
|
||||
}default glob
|
||||
|
||||
|
||||
// A "Checkers" application
|
||||
App.Checkers: App<App.Checkers.State>
|
||||
let img = VoxBox.alloc_capacity(65536*8)
|
||||
App.new<App.Checkers.State>(
|
||||
App.Checkers.init // Estado inicial da aplicação
|
||||
App.Checkers.draw(img) // Conversão do estado para a tela
|
||||
App.Checkers.when // Interação com eventos
|
||||
App.Checkers.tick // Tick O que atualizar no estado global a cada tick
|
||||
App.Checkers.post // Post Como lidar com mensagens do servidor
|
||||
)
|
||||
|
2
base/App/Checkers/Black_Normal.kind
Normal file
2
base/App/Checkers/Black_Normal.kind
Normal file
File diff suppressed because one or more lines are too long
2
base/App/Checkers/Black_Queen.kind
Normal file
2
base/App/Checkers/Black_Queen.kind
Normal file
File diff suppressed because one or more lines are too long
2
base/App/Checkers/Black_Tile.kind
Normal file
2
base/App/Checkers/Black_Tile.kind
Normal file
File diff suppressed because one or more lines are too long
2
base/App/Checkers/Outline.kind
Normal file
2
base/App/Checkers/Outline.kind
Normal file
File diff suppressed because one or more lines are too long
2
base/App/Checkers/Red_Normal.kind
Normal file
2
base/App/Checkers/Red_Normal.kind
Normal file
File diff suppressed because one or more lines are too long
2
base/App/Checkers/Red_Queen.kind
Normal file
2
base/App/Checkers/Red_Queen.kind
Normal file
File diff suppressed because one or more lines are too long
2
base/App/Checkers/White_Tile.kind
Normal file
2
base/App/Checkers/White_Tile.kind
Normal file
File diff suppressed because one or more lines are too long
@ -20,7 +20,7 @@ App.Kind.comp.footer(device: Device, container_layout: Map(String)): DOM
|
||||
DOM.node("div", {}, {}, [
|
||||
App.Kind.comp.list([
|
||||
App.Kind.comp.link_white("Github", footer_font_size, "https://github.com/Kindelia/Kind"),
|
||||
App.Kind.comp.link_white("Telegram", footer_font_size, "https://t.me/formality_lang")
|
||||
App.Kind.comp.link_white("Telegram", footer_font_size, "https://t.me/kindelia")
|
||||
])
|
||||
])
|
||||
])
|
||||
@ -61,4 +61,4 @@ App.Kind.comp.footer(device: Device, container_layout: Map(String)): DOM
|
||||
"display": "flex"
|
||||
"flex-direction": "column"
|
||||
"color": "white"
|
||||
}, [join_us_wrapper, msg_footer_wrapper])
|
||||
}, [join_us_wrapper, msg_footer_wrapper])
|
||||
|
@ -238,7 +238,7 @@ App.RLP.draw(state: App.RLP.State.Local): DOM
|
||||
<p><a href="https://github.com/kind-lang/Kind">
|
||||
`Github`
|
||||
</a></p>
|
||||
<p><a href="https://t.me/formality_lang">
|
||||
<p><a href="https://t.me/kindelia">
|
||||
`Telegram`
|
||||
</a></p>
|
||||
</div>
|
||||
|
39
base/App/Template.kind
Normal file
39
base/App/Template.kind
Normal file
@ -0,0 +1,39 @@
|
||||
App.Template.State: App.State
|
||||
// local global
|
||||
App.State.new(Unit, Unit)
|
||||
|
||||
// Initial state
|
||||
App.Template.init: App.Init<App.Template.State>
|
||||
App.Store.new<App.Template.State>(unit, unit)
|
||||
|
||||
// Render function
|
||||
App.Template.draw: App.Draw<App.Template.State>
|
||||
(state)
|
||||
<div id = "template">"Template"</div>
|
||||
|
||||
// Event handler
|
||||
App.Template.when: App.When<App.Template.State>
|
||||
(event, state)
|
||||
case event {
|
||||
init: App.pass!
|
||||
} default App.pass!
|
||||
|
||||
// Global ticker
|
||||
App.Template.tick: App.Tick<App.Template.State>
|
||||
App.no_tick<App.Template.State>
|
||||
|
||||
// Global visitor
|
||||
App.Template.post: App.Post<App.Template.State>
|
||||
(time, room, addr, data, glob)
|
||||
glob
|
||||
|
||||
|
||||
// A "Template" application
|
||||
App.Template: App<App.Template.State>
|
||||
App.new<App.Template.State>(
|
||||
App.Template.init
|
||||
App.Template.draw
|
||||
App.Template.when
|
||||
App.Template.tick
|
||||
App.Template.post
|
||||
)
|
18
base/Bits/set.kind
Normal file
18
base/Bits/set.kind
Normal file
@ -0,0 +1,18 @@
|
||||
|
||||
Bits.set(idx: Nat, a: Bits, b: Bits): Bits
|
||||
case idx {
|
||||
zero: Bits.set.aux(a, b)
|
||||
succ:
|
||||
case b {
|
||||
e: a
|
||||
i: Bits.i(Bits.set(idx.pred, a, b.pred))
|
||||
o: Bits.o(Bits.set(idx.pred, a, b.pred))
|
||||
}
|
||||
}
|
||||
|
||||
Bits.set.aux(a: Bits, b: Bits): Bits
|
||||
case a {
|
||||
e: b
|
||||
i: Bits.i(Bits.set.aux(a.pred, Bits.drop(1, b)))
|
||||
o: Bits.o(Bits.set.aux(a.pred, Bits.drop(1, b)))
|
||||
}
|
@ -139,7 +139,7 @@ TicTacToe.show(game: TicTacToe):String
|
||||
ts(pc(2,0,gs)) | " | " | ts(pc(2,1,gs)) | " | " | ts(pc(2,2,gs)) | "\n "
|
||||
board
|
||||
|
||||
User.Derenash.TicTacToe.Test: IO<Unit>
|
||||
Tictactoe: _
|
||||
IO {
|
||||
// Prints the initial board
|
||||
let ttt = TicTacToe.init
|
@ -1 +0,0 @@
|
||||
//todo
|
824
base/User/developedby/Problems.kind
Normal file
824
base/User/developedby/Problems.kind
Normal file
@ -0,0 +1,824 @@
|
||||
// How to use this file:
|
||||
// 1. Clone Kind's repo: git clone https://github.com/Kindelia/Kind
|
||||
// 2. Create a dir for you: mkdir Kind/base/User/YourName
|
||||
// 3. Copy that file there: cp Kind/base/Problems.kind Kind/base/User/YourName
|
||||
// 4. Open, uncomment a problem and solve it
|
||||
// 5. Send a PR if you want!
|
||||
// If you need help, read the tutorial on Kind/THEOREMS.md, or ask on Telegram.
|
||||
// Answers: https://github.com/Kindelia/Kind/blob/master/base/User/MaiaVictor/Problems.kind
|
||||
|
||||
// -----------------------------------------------------------------------------
|
||||
|
||||
// ::::::::::::::
|
||||
// :: Programs ::
|
||||
// ::::::::::::::
|
||||
|
||||
// Returns true if both inputs are true
|
||||
Problems.p0(a: Bool, b: Bool): Bool
|
||||
case a b {
|
||||
true true: true
|
||||
} default false
|
||||
|
||||
// Returns true if any input is true
|
||||
Problems.p1(a: Bool, b: Bool): Bool
|
||||
case a b {
|
||||
false false: false
|
||||
} default true
|
||||
|
||||
// Returns true if both inputs are identical
|
||||
Problems.p2(a: Bool, b: Bool): Bool
|
||||
case a b {
|
||||
false false: true
|
||||
true true : true
|
||||
} default false
|
||||
|
||||
// Returns the first element of a pair
|
||||
Problems.p3<A: Type, B: Type>(pair: Pair<A,B>): A
|
||||
open pair
|
||||
pair.fst
|
||||
|
||||
// Returns the second element of a pair
|
||||
Problems.p4<A: Type, B: Type>(pair: Pair<A,B>): B
|
||||
open pair
|
||||
pair.snd
|
||||
|
||||
// Inverses the order of the elements of a pair
|
||||
Problems.p5<A: Type, B: Type>(pair: Pair<A,B>): Pair<B,A>
|
||||
open pair
|
||||
{pair.snd, pair.fst}
|
||||
|
||||
// Applies a function to both elements of a Pair
|
||||
Problems.p6<A: Type, B: Type>(fn: A -> B, pair: Pair<A,A>): Pair<B,B>
|
||||
open pair
|
||||
{fn(pair.fst), fn(pair.snd)}
|
||||
|
||||
// Doubles a number
|
||||
Problems.p7(n: Nat): Nat
|
||||
case n {
|
||||
// 0 * 2 == 0
|
||||
zero: 0
|
||||
// 2 + 2*(n-1) == 2 + 2n - 2 == 2n
|
||||
succ: Nat.succ(Nat.succ(Problems.p7(n.pred)))
|
||||
}
|
||||
|
||||
// Halves a number, rounding down
|
||||
Problems.p8(n: Nat): Nat
|
||||
case n {
|
||||
zero: 0
|
||||
succ: case n.pred {
|
||||
zero: 0
|
||||
// n/2 == 1 + (n-2)/2
|
||||
succ: Nat.succ(Problems.p8(n.pred.pred))
|
||||
}
|
||||
}
|
||||
|
||||
// Adds two numbers
|
||||
Problems.p9(a: Nat, b: Nat): Nat
|
||||
case a {
|
||||
// 0 ++ b == b
|
||||
zero: b
|
||||
// a + b == (a-1) + (b+1)
|
||||
succ: Problems.p9(a.pred, Nat.succ(b))
|
||||
}
|
||||
|
||||
// Subtracts two numbers
|
||||
Problems.p10(a: Nat, b: Nat): Nat
|
||||
case a b {
|
||||
// 0 - 0 == 0
|
||||
zero zero: 0
|
||||
// 0 - b == 0
|
||||
zero succ: 0
|
||||
// a - 0 == a
|
||||
succ zero: a
|
||||
// a - b == (a-1) - (b-1)
|
||||
succ succ: Problems.p10(a.pred, b.pred)
|
||||
}
|
||||
|
||||
// Multiplies two numbers
|
||||
Problems.p11(a: Nat, b: Nat): Nat
|
||||
case a {
|
||||
// 0 * b == b
|
||||
zero: 0
|
||||
// a * b == ((a-1) * b) + b
|
||||
succ: Problems.p9(Problems.p11(a.pred, b), b)
|
||||
}
|
||||
|
||||
// Returns true if a < b
|
||||
Problems.p12(a: Nat, b: Nat): Bool
|
||||
case a b {
|
||||
// 0 not smaller than 0
|
||||
zero zero: false
|
||||
// 0 smaller than x+1
|
||||
zero succ: true
|
||||
// x+1 not smaller than 0
|
||||
succ zero: false
|
||||
// (a < b) == ((a-1) < (b-1))
|
||||
succ succ: Problems.p12(a.pred, b.pred)
|
||||
}
|
||||
|
||||
// Returns true if a == b
|
||||
Problems.p13(a: Nat, b: Nat): Bool
|
||||
case a b {
|
||||
zero zero: true
|
||||
zero succ: false
|
||||
succ zero: false
|
||||
// (a = b) == ((a-1) = (b-1))
|
||||
succ succ: Problems.p13(a.pred, b.pred)
|
||||
}
|
||||
|
||||
// Returns the first element of a List
|
||||
Problems.p14<A: Type>(xs: List<A>): Maybe<A>
|
||||
case xs {
|
||||
nil : none
|
||||
cons: some(xs.head)
|
||||
}
|
||||
|
||||
// Returns the list without the first element
|
||||
Problems.p15<A: Type>(xs: List<A>): List<A>
|
||||
case xs {
|
||||
nil : []
|
||||
cons: xs.tail
|
||||
}
|
||||
|
||||
// Returns the length of a list
|
||||
Problems.p16<A: Type>(xs: List<A>): Nat
|
||||
case xs {
|
||||
nil : 0
|
||||
cons: Nat.succ(Problems.p16!(xs.tail))
|
||||
}
|
||||
|
||||
// Many poorly optimized funcions below (not tail-recursive, assintotically bad, etc)
|
||||
|
||||
// Concatenates two lists
|
||||
Problems.p17<A: Type>(xs: List<A>, ys: List<A>): List<A>
|
||||
case xs {
|
||||
nil : ys
|
||||
cons: xs.head & Problems.p17!(xs.tail, ys)
|
||||
}
|
||||
|
||||
// Applies a function to all elements of a list
|
||||
Problems.p18<A: Type, B: Type>(fn: A -> B, xs: List<A>): List<B>
|
||||
case xs {
|
||||
nil : []
|
||||
cons: fn(xs.head) & Problems.p18!!(fn, xs.tail)
|
||||
}
|
||||
|
||||
// Returns the same list, with the order reversed
|
||||
Problems.p19<A: Type>(xs: List<A>): List<A>
|
||||
case xs {
|
||||
nil : []
|
||||
// O(n²)?
|
||||
cons: Problems.p19!(xs.tail) ++ [xs.head]
|
||||
}
|
||||
|
||||
// Returns pairs of the elements of the 2 input lists on the same index
|
||||
// Ex: Problems.p20!!([1,2], ["a","b"]) == [{1,"a"},{2,"b"}]
|
||||
Problems.p20<A: Type, B: Type>(xs: List<A>, ys: List<B>): List<Pair<A,B>>
|
||||
case xs ys {
|
||||
cons cons: {xs.head, ys.head} & Problems.p20!!(xs.tail, ys.tail)
|
||||
} default []
|
||||
|
||||
|
||||
// Returns the smallest element of a List
|
||||
Problems.p21.go(xs: List<Nat>, min: Nat): Nat
|
||||
case xs {
|
||||
nil : min
|
||||
cons:
|
||||
let new_min = if xs.head <? min then xs.head else min
|
||||
Problems.p21.go(xs.tail, new_min)
|
||||
}
|
||||
|
||||
Problems.p21(xs: List<Nat>): Nat
|
||||
case xs {
|
||||
nil : 0
|
||||
cons: Problems.p21.go(xs.tail, xs.head)
|
||||
}
|
||||
|
||||
// Returns the same list without the smallest element and the smallest element
|
||||
// (Original problem didn't return smallest, but i wanted to use it on p23)
|
||||
// Peguei a ideia desse video e quebrei em 2 listas, acho que é mais facil de entender
|
||||
// https://www.youtube.com/watch?v=rvb70cZS-ao
|
||||
Problems.p22.go(
|
||||
xs: List<Nat>
|
||||
heads: List<Nat> -> List<Nat>
|
||||
tails: List<Nat> -> List<Nat>
|
||||
min: Nat
|
||||
): Pair<List<Nat>, Nat>
|
||||
case xs {
|
||||
nil : {heads(tails([])), min}
|
||||
cons:
|
||||
if xs.head <? min then
|
||||
Problems.p22.go(
|
||||
xs.tail,
|
||||
(h) heads(min & tails(h)),
|
||||
(t) t,
|
||||
xs.head
|
||||
)
|
||||
else
|
||||
Problems.p22.go(
|
||||
xs.tail,
|
||||
heads,
|
||||
(t) tails(xs.head & t),
|
||||
min
|
||||
)
|
||||
}
|
||||
// [1 2 3 0 4 5]
|
||||
// [2 3 0 4 5] [h] [t] 1
|
||||
// [3 0 4 5] [h] [2 t] 1
|
||||
// [0 4 5] [h] [2 3 t] 1
|
||||
// [4 5] [1 2 3 h] [t] 0
|
||||
// [5] [1 2 3 h] [4 t] 0
|
||||
// [] [1 2 3 h] [4 5 t] 0
|
||||
// [1 2 3 4 5]
|
||||
|
||||
Problems.p22(xs: List<Nat>): Pair<List<Nat>, Nat>
|
||||
case xs {
|
||||
nil : {[], 0}
|
||||
cons: Problems.p22.go(xs.tail, (h) h, (t) t, xs.head)
|
||||
}
|
||||
|
||||
// Returns the same list, in ascending order
|
||||
Problems.p23.go(
|
||||
xs: List<Nat>,
|
||||
acc: List<Nat> -> List<Nat>
|
||||
): List<Nat>
|
||||
case xs {
|
||||
nil : acc([])
|
||||
cons:
|
||||
let {xs_cut, min} = Problems.p22(xs)
|
||||
Problems.p23.go(xs_cut, (e) acc(min & e))
|
||||
}
|
||||
|
||||
Problems.p23(xs: List<Nat>): List<Nat>
|
||||
Problems.p23.go(xs, (e) e)
|
||||
|
||||
// -----------------------------------------------------------------------------
|
||||
|
||||
// ::::::::::::::
|
||||
// :: Theorems ::
|
||||
// ::::::::::::::
|
||||
|
||||
// Note: these problems use functions from the base libs, NOT the ones above
|
||||
|
||||
// Aliases
|
||||
Chain: _
|
||||
Equal.chain
|
||||
|
||||
Rev: _
|
||||
List.reverse
|
||||
|
||||
Rev.go: _
|
||||
List.reverse.go
|
||||
|
||||
|
||||
// true is true
|
||||
Problems.t0: true == true
|
||||
refl
|
||||
|
||||
// "false" short-circuits "and" on first position
|
||||
Problems.t1(a: Bool): Bool.and(false, a) == false
|
||||
refl
|
||||
|
||||
// "false" short-circuits "and" on second position
|
||||
Problems.t2(a: Bool): Bool.and(a, false) == false
|
||||
case a {
|
||||
false: refl
|
||||
true : refl
|
||||
}!
|
||||
|
||||
// "true" short-circuits "or" on first position
|
||||
Problems.t3(a: Bool): Bool.or(true, a) == true
|
||||
refl
|
||||
|
||||
// "true" short-circuits "or" on second position
|
||||
Problems.t4(a: Bool): Bool.or(a, true) == true
|
||||
case a {
|
||||
false: refl
|
||||
true : refl
|
||||
}!
|
||||
|
||||
// a is always equal to a
|
||||
Problems.t5(a: Bool): Bool.eql(a, a) == true
|
||||
case a {
|
||||
false: refl
|
||||
true : refl
|
||||
}!
|
||||
|
||||
// Double negation changes nothing
|
||||
Problems.t6(a: Bool): Bool.not(Bool.not(a)) == a
|
||||
case a {
|
||||
false: refl
|
||||
true : refl
|
||||
}!
|
||||
|
||||
// de Morgan: nand is or(not, not)
|
||||
Problems.t7(
|
||||
a: Bool,
|
||||
b: Bool
|
||||
): Bool.not(Bool.and(a,b)) == Bool.or(Bool.not(a), Bool.not(b))
|
||||
case a b {
|
||||
false false: refl
|
||||
false true : refl
|
||||
true false: refl
|
||||
true true : refl
|
||||
}!
|
||||
|
||||
// de Morgan: nor is and(not, not)
|
||||
Problems.t8(
|
||||
a: Bool,
|
||||
b: Bool
|
||||
): Bool.not(Bool.or(a,b)) == Bool.and(Bool.not(a), Bool.not(b))
|
||||
case a b {
|
||||
false false: refl
|
||||
false true : refl
|
||||
true false: refl
|
||||
true true : refl
|
||||
}!
|
||||
|
||||
// Taking first and second from pair and putting them back together changes nothing
|
||||
Problems.t9(
|
||||
a: Pair<Nat,Nat>
|
||||
): Pair.new<Nat,Nat>(Pair.fst<Nat,Nat>(a), Pair.snd<Nat,Nat>(a)) == a
|
||||
case a {
|
||||
new: refl
|
||||
}!
|
||||
|
||||
// Swapping pair twice changes nothing
|
||||
Problems.t10(a: Pair<Nat,Nat>): Pair.swap<Nat,Nat>(Pair.swap<Nat,Nat>(a)) == a
|
||||
case a {
|
||||
new: refl
|
||||
}!
|
||||
|
||||
// every number is same as itself
|
||||
Problems.t11(n: Nat): Nat.same(n) == n
|
||||
case n {
|
||||
zero: refl
|
||||
succ:
|
||||
let h = Problems.t11(n.pred)
|
||||
apply(Nat.succ, h)
|
||||
}!
|
||||
|
||||
// halving the double changes nothing
|
||||
Problems.t12(n: Nat): Nat.half(Nat.double(n)) == n
|
||||
case n {
|
||||
zero: refl
|
||||
succ:
|
||||
let h = Problems.t12(n.pred)
|
||||
apply(Nat.succ, h)
|
||||
}!
|
||||
|
||||
// 0 is identity of addition, first position
|
||||
Problems.t13(n: Nat): Nat.add(0, n) == n
|
||||
refl
|
||||
|
||||
// 0 is identity of addition, second position
|
||||
Problems.t14(n: Nat): Nat.add(n, 0) == n
|
||||
case n {
|
||||
zero: refl
|
||||
succ:
|
||||
let h = Problems.t14(n.pred)
|
||||
apply(Nat.succ, h)
|
||||
}!
|
||||
|
||||
// Don't know a good description, maybe distributes to addition
|
||||
// Addition is associative with successor, first position
|
||||
Problems.t15(n: Nat, m: Nat): Nat.add(Nat.succ(n),m) == Nat.succ(Nat.add(n,m))
|
||||
case n {
|
||||
zero: refl
|
||||
succ:
|
||||
let h = Problems.t15(n.pred, m)
|
||||
apply(Nat.succ, h)
|
||||
}!
|
||||
|
||||
// Addition is associative with successor, second position
|
||||
Problems.t16(n: Nat, m: Nat): Nat.add(n,Nat.succ(m)) == Nat.succ(Nat.add(n,m))
|
||||
case n {
|
||||
zero: refl
|
||||
succ:
|
||||
let h = Problems.t16(n.pred, m)
|
||||
apply(Nat.succ, h)
|
||||
}!
|
||||
|
||||
// Addition is commutative on the identity
|
||||
Problems.t17.aux(n: Nat): (0 + n) == (n + 0)
|
||||
let a = Problems.t13(n)
|
||||
let b = mirror(Problems.t14(n))
|
||||
Chain!!!!(a, b)
|
||||
|
||||
// Addition is commutative
|
||||
Problems.t17(n: Nat, m: Nat): Nat.add(n, m) == Nat.add(m, n)
|
||||
case n {
|
||||
zero: Problems.t17.aux(m)
|
||||
succ:
|
||||
let e0 = Problems.t15(n.pred, m)
|
||||
let h = Problems.t17(n.pred, m)
|
||||
let a = apply(Nat.succ, h)
|
||||
let e1 = mirror(Problems.t16(m, n.pred))
|
||||
Chain!!!!(Chain!!!!(e0, a), e1)
|
||||
}!
|
||||
|
||||
Problems.t18.aux(
|
||||
n: Nat
|
||||
): (Nat.succ(n) + Nat.succ(n)) == Nat.succ(Nat.succ(n + n))
|
||||
apply(Nat.succ, Problems.t16(n, n))
|
||||
|
||||
// Equivalency between addition and doubling
|
||||
Problems.t18(n: Nat): Nat.add(n,n) == Nat.double(n)
|
||||
case n {
|
||||
zero: refl
|
||||
succ:
|
||||
let h = Problems.t18(n.pred)
|
||||
let a = apply((val) Nat.succ(Nat.succ(val)), h)
|
||||
let e = Problems.t18.aux(n.pred)
|
||||
Chain!!!!(e, a)
|
||||
}!
|
||||
|
||||
// A number is always smaller than its successor
|
||||
Problems.t19(n: Nat): Nat.ltn(n, Nat.succ(n)) == true
|
||||
case n {
|
||||
zero: refl
|
||||
succ: Problems.t19(n.pred)
|
||||
}!
|
||||
|
||||
// A number's successor is always greater than itself
|
||||
Problems.t20(n: Nat): Nat.gtn(Nat.succ(n), n) == true
|
||||
case n {
|
||||
zero: refl
|
||||
succ: Problems.t20(n.pred)
|
||||
}!
|
||||
|
||||
// n-n is 0
|
||||
Problems.t21(n: Nat): Nat.sub(n,n) == 0
|
||||
case n {
|
||||
zero: refl
|
||||
succ: Problems.t21(n.pred)
|
||||
}!
|
||||
|
||||
//If n is 1, then S(n) is 2
|
||||
Problems.t22(n: Nat, e: n == 1): Nat.succ(n) == 2
|
||||
apply(Nat.succ, e)
|
||||
|
||||
// If n ?= m, then n is m
|
||||
Problems.t23(n: Nat, m: Nat, e: Nat.eql(n,m) == true): n == m
|
||||
case n with e {
|
||||
zero: case m with e {
|
||||
zero:
|
||||
refl
|
||||
succ:
|
||||
let contra = Bool.false_neq_true(e)
|
||||
Empty.absurd!(contra)
|
||||
}!
|
||||
succ: case m with e {
|
||||
zero:
|
||||
let contra = Bool.false_neq_true(e)
|
||||
Empty.absurd!(contra)
|
||||
succ:
|
||||
let h = Problems.t23(n.pred, m.pred, e)
|
||||
apply(Nat.succ, h)
|
||||
}!
|
||||
}!
|
||||
|
||||
// the length of a list with at least one element is greater than zero
|
||||
Problems.t24(
|
||||
xs: List<Nat>
|
||||
): Nat.gtn(List.length<Nat>(List.cons<Nat>(1,xs)),0) == true
|
||||
case xs {
|
||||
nil : refl
|
||||
cons: Problems.t24(xs.tail)
|
||||
}!
|
||||
|
||||
// Mapping a list with the identity function changes nothing
|
||||
Problems.t25(xs: List<Nat>): List.map<Nat,Nat>((x) x, xs) == xs
|
||||
case xs {
|
||||
nil : refl
|
||||
cons: apply(List.cons!(xs.head), Problems.t25(xs.tail))
|
||||
}!
|
||||
|
||||
// The length of two concatenated lists is the sum of each list's length
|
||||
Problems.t26(
|
||||
xs: List<Nat>,
|
||||
ys: List<Nat>
|
||||
): (List.length<Nat>(xs) + List.length<Nat>(ys)) == List.length<Nat>(List.concat<Nat>(xs,ys))
|
||||
case xs {
|
||||
nil : refl
|
||||
cons: apply(Nat.succ, Problems.t26(xs.tail, ys))
|
||||
}!
|
||||
|
||||
|
||||
// Auxiliary proofs for t27 (reverse(reverse(xs)) == xs)
|
||||
|
||||
CatAssociative<A: Type>(
|
||||
xs: List<A>
|
||||
ys: List<A>
|
||||
zs: List<A>
|
||||
): (xs ++ (ys ++ zs)) == ((xs ++ ys) ++ zs)
|
||||
case xs {
|
||||
nil: refl
|
||||
cons: apply((e) xs.head & e, CatAssociative!(xs.tail, ys, zs))
|
||||
}!
|
||||
|
||||
CatNilRight<A: Type>(xs: List<A>): (xs ++ []) == xs
|
||||
case xs {
|
||||
nil : refl
|
||||
cons: apply((e) xs.head & e, CatNilRight<A>(xs.tail))
|
||||
}!
|
||||
|
||||
RevGoStep<A: Type>(
|
||||
n : A
|
||||
xs: List<A>
|
||||
ys: List<A>
|
||||
): Rev.go<A>(n & xs, ys) == Rev.go<A>(xs, n & ys)
|
||||
refl
|
||||
|
||||
// Second argument of rev.go can be taken out with a concat
|
||||
// Alternatively, Rev.go cats the reverse of the first with the second
|
||||
RevGoCatYs<A: Type>(
|
||||
xs: List<A>,
|
||||
ys: List<A>
|
||||
): Rev.go<A>(xs, ys) == (Rev.go<A>(xs, List.nil<A>) ++ ys)
|
||||
case xs {
|
||||
nil : refl
|
||||
cons:
|
||||
// 1: go(head & tail, ys) == go(tail, head & ys)
|
||||
// 2: go(tail, head & ys) == go(tail, []) ++ (head & ys)
|
||||
// 3: go(tail, []) ++ (head & ys) == go(tail, []) ++ ([head] ++ ys)
|
||||
// 4: go(tail, []) ++ ([head] ++ ys) == (go(tail, []) ++ [head]) ++ ys
|
||||
// 5: (go(tail, []) ++ [head]) ++ ys == go(tail, [head]) ++ ys
|
||||
// 6: go(tail, [head]) ++ ys == go(head & tail) ++ ys
|
||||
// --------------------------------------------------------------------
|
||||
// go(head & tail, ys) == go(head & tail) ++ ys
|
||||
|
||||
let t1 = RevGoStep<A>(xs.head, xs.tail, ys)
|
||||
|
||||
// Is this inductive step correct?
|
||||
// Isn't it assuming the thesis?
|
||||
// Isn't this like a fake recursion on ys?
|
||||
// This is not proving that if it works with length(xs) it works with length(xs)+1
|
||||
// I took the idea from a different proof made for Idris that I saw online
|
||||
// reverseReverseOnto from https://github.com/idris-lang/Idris2/blob/main/libs/base/Data/List.idr
|
||||
let t2 = RevGoCatYs<A>(xs.tail, xs.head & ys)
|
||||
|
||||
let t3 = refl :: (xs.head & ys) == ([xs.head] ++ ys)
|
||||
let t3 = apply((e) Rev.go!(xs.tail, []) ++ e, t3)
|
||||
|
||||
let t4 = CatAssociative<A>(Rev.go!(xs.tail, []), [xs.head], ys)
|
||||
|
||||
// This is t2 when ys is nil, which must hold
|
||||
let t5 = RevGoCatYs<A>(xs.tail, [xs.head]) // go(tail, [head]) == go(tail, []) ++ [head]
|
||||
let t5 = mirror(t5)
|
||||
let t5 = apply((e) e ++ ys, t5)
|
||||
|
||||
let t6 = mirror(RevGoStep<A>(xs.head, xs.tail, []))
|
||||
let t6 = apply((e) e ++ ys, t6)
|
||||
|
||||
Chain!!!!(t1, Chain!!!!(t2, Chain!!!!(t3, Chain!!!!(t4, Chain!!!!(t5, t6)))))
|
||||
}!
|
||||
|
||||
// First element becomes last when list is reversed
|
||||
RevGoHeadGoesLast<A: Type>(
|
||||
n: A
|
||||
xs: List<A>
|
||||
): Rev.go<A>(n & xs, []) == (Rev.go<A>(xs, []) ++ [n])
|
||||
// 1: go(n & xs, []) == go(xs, [n])
|
||||
// 2: go(xs, [n]) == go(xs, []) ++ [n]
|
||||
let t1 = RevGoStep!(n, xs, [])
|
||||
let t2 = RevGoCatYs!(xs, [n])
|
||||
Chain!!!!(t1, t2)
|
||||
|
||||
|
||||
//Reversing a cat is the same as cating both lists reverted, in opposite order
|
||||
RevGoContraDistributive<A: Type>(
|
||||
xs: List<A>
|
||||
ys: List<A>
|
||||
): Rev.go<A>(List.concat<A>(xs, ys), List.nil<A>)
|
||||
== List.concat<A>(Rev.go<A>(ys, List.nil<A>), Rev.go<A>(xs, List.nil<A>))
|
||||
// go(xs ++ ys, []) == go(ys, []) ++ go(xs, [])
|
||||
case xs {
|
||||
nil:
|
||||
// 1: go([] ++ ys, []) == go(ys, [])
|
||||
// 2: go(ys, []) == go(ys, []) ++ []
|
||||
let t1 = refl :: Rev.go<A>([] ++ ys, []) == Rev.go<A>(ys, [])
|
||||
let t2 = mirror(CatNilRight<A>(Rev.go!(ys, [])))
|
||||
Chain!!!!(t1, t2)
|
||||
cons:
|
||||
// 1: go((head & tail) ++ ys, []) == go(head & (tail ++ ys), [])
|
||||
// 2: go(head & (tail ++ ys), []) == go(tail ++ ys, []) ++ [head]
|
||||
// 3: go(tail ++ ys, []) ++ [head] == (go(ys, []) ++ go(tail, [])) ++ [head]
|
||||
// 4: (go(ys, []) ++ go(tail, [])) ++ [head] == go(ys, []) ++ (go(tail, []) ++ [head])
|
||||
// 5: go(ys, []) ++ (go(tail, []) ++ [head]) == go(ys, []) ++ go(head & tail, [])
|
||||
// -------------------------------------------------------------------------------
|
||||
// go((head & tail) ++ ys, []) == go(ys, []) ++ go(head & tail, [])
|
||||
let t1 = refl ::
|
||||
Rev.go<A>((xs.head & xs.tail) ++ ys, []) ==
|
||||
Rev.go<A>(xs.head & (xs.tail ++ ys), [])
|
||||
|
||||
let t2 = RevGoHeadGoesLast<A>(xs.head, xs.tail ++ ys)
|
||||
|
||||
let t3 = RevGoContraDistributive<A>(xs.tail, ys)
|
||||
let t3 = apply((e) e ++ [xs.head], t3)
|
||||
|
||||
let t4 = CatAssociative<A>(
|
||||
Rev.go<A>(ys, []),
|
||||
Rev.go<A>(xs.tail, []),
|
||||
[xs.head])
|
||||
let t4 = mirror(t4)
|
||||
|
||||
let t5 = mirror(RevGoHeadGoesLast<A>(xs.head, xs.tail))
|
||||
let t5 = apply((e) Rev.go<A>(ys, []) ++ e, t5)
|
||||
|
||||
Chain!!!!(t1, Chain!!!!(t2, Chain!!!!(t3, Chain!!!!(t4, t5))))
|
||||
}!
|
||||
|
||||
ReverseReverse<A: Type>(
|
||||
xs: List<A>
|
||||
): Rev<A>(Rev<A>(xs)) == xs
|
||||
case xs {
|
||||
nil : refl
|
||||
cons:
|
||||
// 1: rev(rev(head & tail)) == go(go(head & tail, []), [])
|
||||
// 2: go(go(head & tail, []), []) == go(go(tail, []) ++ [head], [])
|
||||
// 3: go(go(tail, []) ++ [head], []) == go([head], []) ++ go(go(tail, []))
|
||||
// 4: go([head], []) ++ go(go(tail, [])) == go([head], []) ++ tail
|
||||
// 5: go([head], []) ++ tail == [head] ++ tail
|
||||
// 6: [head] ++ tail == head & tail
|
||||
// ---------------------------------------------------------------------------
|
||||
// rev(rev(head & tail)) == head & tail
|
||||
let t1 = refl ::
|
||||
Rev<A>(Rev<A>(xs.head & xs.tail)) ==
|
||||
Rev.go<A>(Rev.go<A>(xs.head & xs.tail, []), [])
|
||||
|
||||
let t2 = RevGoHeadGoesLast<A>(xs.head, xs.tail)
|
||||
let t2 = apply((e) Rev.go<A>(e, []), t2)
|
||||
|
||||
let t3 = RevGoContraDistributive<A>(Rev.go<A>(xs.tail, []), [xs.head])
|
||||
|
||||
let t4 = ReverseReverse<A>(xs.tail)
|
||||
let t4 = apply((e) Rev.go<A>([xs.head], []) ++ e, t4)
|
||||
|
||||
let t5 = refl :: Rev.go<A>([xs.head], []) == [xs.head]
|
||||
let t5 = apply((e) e ++ xs.tail, t5)
|
||||
|
||||
let t6 = refl :: ([xs.head] ++ xs.tail) == (xs.head & xs.tail)
|
||||
|
||||
Chain!!!!(t1, Chain!!!!(t2, Chain!!!!(t3, Chain!!!!(t4, Chain!!!!(t5, t6)))))
|
||||
}!
|
||||
|
||||
// Reversing twice changes nothing
|
||||
Problems.t27(
|
||||
xs: List<Nat>
|
||||
): Rev<Nat>(Rev<Nat>(xs)) == xs
|
||||
ReverseReverse<Nat>(xs)
|
||||
|
||||
// Alternative proof theorem 27 (taken from Idris)
|
||||
|
||||
// Applying reverse on reverse.go swaps xs with ys
|
||||
ReverseSwapsReverseGo<A: Type>(
|
||||
xs: List<A>
|
||||
ys: List<A>
|
||||
): Rev.go<A>(Rev.go<A>(xs, ys), []) == Rev.go<A>(ys, xs)
|
||||
case xs {
|
||||
nil : refl
|
||||
cons:
|
||||
// go(go(head & tail, ys), []) == go(go(tail, head & ys), [])
|
||||
// go(go(tail, head & ys), []) == go(head & ys, tail)
|
||||
// go(head & ys, tail) == go(ys, head & tail)
|
||||
|
||||
let t1 = RevGoStep<A>(xs.head, xs.tail, ys)
|
||||
let t1 = apply((e) Rev.go<A>(e, []), t1)
|
||||
|
||||
let t2 = ReverseSwapsReverseGo<A>(xs.tail, xs.head & ys)
|
||||
|
||||
let t3 = RevGoStep<A>(xs.head, ys, xs.tail)
|
||||
|
||||
Chain!!!!(t1, Chain!!!!(t2, t3))
|
||||
}!
|
||||
|
||||
ReverseReverseAlt<A: Type>(
|
||||
xs: List<A>
|
||||
ys: List<A>
|
||||
): Rev.go<A>(Rev.go<A>(xs, []), []) == xs
|
||||
ReverseSwapsReverseGo<A>(xs, [])
|
||||
|
||||
|
||||
// Theorems continue
|
||||
|
||||
// true is not false
|
||||
Problems.t28: true != false
|
||||
(e) Bool.true_neq_false(e)
|
||||
|
||||
// 3 is not 2
|
||||
Problems.t29: 3 != 2
|
||||
(e)
|
||||
let a = apply(Nat.eql(2), e)
|
||||
Bool.false_neq_true(a)
|
||||
|
||||
// An "or" with "true" in the first position is never false
|
||||
Problems.t30(a: Bool): Bool.or(true, a) != false
|
||||
(e)
|
||||
let t = Chain!!!!(mirror(Problems.t3(a)), e)
|
||||
Bool.true_neq_false(t)
|
||||
|
||||
// An "or" with "true" in the second position is never false
|
||||
Problems.t31(a: Bool): Bool.or(a, true) != false
|
||||
(e)
|
||||
let t = Chain!!!!(mirror(Problems.t4(a)), e)
|
||||
Bool.true_neq_false(t)
|
||||
|
||||
// An "and" with "false" in the first position is never true
|
||||
Problems.t32(a: Bool): Bool.and(false, a) != true
|
||||
(e)
|
||||
let t = Chain!!!!(mirror(Problems.t1(a)), e)
|
||||
Bool.false_neq_true(t)
|
||||
|
||||
// An "and" with "false" in the secind position is never true
|
||||
Problems.t33(a: Bool): Bool.and(a, false) != true
|
||||
(e)
|
||||
let t = Chain!!!!(mirror(Problems.t2(a)), e)
|
||||
Bool.false_neq_true(t)
|
||||
|
||||
// Equality is commutative
|
||||
Problems.t34(a: Nat, b: Nat, e: a == b): b == a
|
||||
// Kinda cheating, the actual proof is the definition of mirror (which also works for any type)
|
||||
mirror(e)
|
||||
|
||||
// Equality is transitive
|
||||
Problems.t35(a: Nat, b: Nat, c: Nat, e0: a == b, e1: b == c): a == c
|
||||
// Cheating again
|
||||
Chain!!!!(e0, e1)
|
||||
|
||||
// P could be returning any type, so we don't know the concrete value of P(Nat.same(a))
|
||||
// But since same(a)==a, P(Nat.same(a)) must be P(a)
|
||||
// If we can show that to the typechecker, we can just return p which already has the correct type
|
||||
Problems.t36(a: Nat, P: Nat -> Type, p: P(a)): P(Nat.same(a))
|
||||
// t11 shows that same(a)==a
|
||||
// We use it to rewrite the type of p to P(same(a)) since both are the same
|
||||
// mirror cause we need a -> same(a)
|
||||
p :: rewrite x in P(x) with mirror(Problems.t11(a))
|
||||
|
||||
Problems:_
|
||||
let p0 = Problems.p0(true, true)
|
||||
let p1 = Problems.p1(true, false)
|
||||
let p2 = Problems.p2(false, false)
|
||||
let p3 = Problems.p3!!({1, "second"})
|
||||
let p4 = Problems.p4!!({1, "second"})
|
||||
let p5 = Problems.p5!!({1, "second"})
|
||||
let p6 = Problems.p6<Nat, String>(Nat.show, {1, 2})
|
||||
let p7 = Problems.p7(5)
|
||||
let p8 = Problems.p8(9)
|
||||
let p9 = Problems.p9(5, 13)
|
||||
let p10 = Problems.p10(45, 31)
|
||||
let p11 = Problems.p11(8, 35)
|
||||
let p12 = Problems.p12(3, 29)
|
||||
let p13 = Problems.p13(8, 8)
|
||||
let p14 = Problems.p14!([6 4 23 7 9 4 2 7 0])
|
||||
let p15 = Problems.p15!([6 4 23 7 9 4 2 7 0])
|
||||
let p16 = Problems.p16!([6 4 23 7 9 4 2 7 0])
|
||||
let p17 = Problems.p17!([6 4 23 7 9] [4 2 7 0])
|
||||
let p18 = Problems.p18!!(Nat.show, [6 4 23 7 9 4 2 7 0])
|
||||
let p19 = Problems.p19!([6 4 23 7 9 4 2 7 0])
|
||||
let p20 = Problems.p20!!([1 2], ["1" "2" "3" "4" "5"])
|
||||
let p21 = Problems.p21([6 4 23 7 9 4 2 7 0])
|
||||
let p22 = Problems.p22([6 4 23 7 9 4 2 7 0 0])
|
||||
let p23 = Problems.p23([6 4 23 7 9 4 2 7 0])
|
||||
|
||||
let t0 = Problems.t0
|
||||
let t1 = Problems.t1
|
||||
let t2 = Problems.t2
|
||||
let t3 = Problems.t3
|
||||
let t4 = Problems.t4
|
||||
let t5 = Problems.t5
|
||||
let t6 = Problems.t6
|
||||
let t7 = Problems.t7
|
||||
let t8 = Problems.t8
|
||||
let t9 = Problems.t9
|
||||
let t10 = Problems.t10
|
||||
let t11 = Problems.t11
|
||||
let t12 = Problems.t12
|
||||
let t13 = Problems.t13
|
||||
let t14 = Problems.t14
|
||||
let t15 = Problems.t15
|
||||
let t16 = Problems.t16
|
||||
let t17 = Problems.t17
|
||||
let t18 = Problems.t18
|
||||
let t19 = Problems.t19
|
||||
let t20 = Problems.t20
|
||||
let t21 = Problems.t21
|
||||
let t22 = Problems.t22
|
||||
let t23 = Problems.t23
|
||||
let t24 = Problems.t24
|
||||
let t25 = Problems.t25
|
||||
let t26 = Problems.t26
|
||||
let t27 = Problems.t27
|
||||
let t28 = Problems.t28
|
||||
let t29 = Problems.t29
|
||||
let t30 = Problems.t30
|
||||
let t31 = Problems.t31
|
||||
let t32 = Problems.t32
|
||||
let t33 = Problems.t33
|
||||
let t34 = Problems.t34
|
||||
let t35 = Problems.t35
|
||||
let t36 = Problems.t36
|
||||
|
||||
// p0
|
||||
// List.show!(Nat.show, p23)
|
||||
?problems
|
497
base/User/gzsr/Problems.kind
Normal file
497
base/User/gzsr/Problems.kind
Normal file
@ -0,0 +1,497 @@
|
||||
// How to use this file:
|
||||
// 1. Clone Kind's repo: git clone https://github.com/Kindelia/Kind
|
||||
// 2. Create a dir for you: mkdir Kind/base/User/YourName
|
||||
// 3. Copy that file there: cp Kind/base/Problems.kind Kind/base/User/YourName
|
||||
// 4. Open, uncomment a problem and solve it
|
||||
// 5. Send a PR if you want!
|
||||
// If you need help, read the tutorial on Kind/THEOREMS.md, or ask on Telegram.
|
||||
// Answers: https://github.com/Kindelia/Kind/blob/master/base/User/MaiaVictor/Problems.kind
|
||||
|
||||
// -----------------------------------------------------------------------------
|
||||
|
||||
// ::::::::::::::
|
||||
// :: Programs ::
|
||||
// ::::::::::::::
|
||||
|
||||
// Returs true if both inputs are true
|
||||
Problems.p0(a: Bool, b: Bool): Bool
|
||||
case a {
|
||||
true: b
|
||||
false: false
|
||||
}
|
||||
|
||||
// Returs true if any input is true
|
||||
Problems.p1(a: Bool, b: Bool): Bool
|
||||
case a b {
|
||||
false false : false
|
||||
} default true
|
||||
|
||||
|
||||
// Returs true if both inputs are identical
|
||||
Problems.p2(a: Bool, b: Bool): Bool
|
||||
case a b {
|
||||
true true : true
|
||||
false false : true
|
||||
} default false
|
||||
|
||||
|
||||
// Returns the second element of a pair
|
||||
Problems.p3<A: Type, B: Type>(pair: Pair<A,B>): A
|
||||
case pair {
|
||||
new: pair.fst
|
||||
}
|
||||
|
||||
|
||||
// Returns the second element of a pair
|
||||
Problems.p4<A: Type, B: Type>(pair: Pair<A,B>): B
|
||||
case pair {
|
||||
new: pair.snd
|
||||
}
|
||||
|
||||
|
||||
// Inverses the order of the elements of a pair
|
||||
Problems.p5<A: Type, B: Type>(pair: Pair<A,B>): Pair<B,A>
|
||||
case pair {
|
||||
new : Pair.new!!(pair.snd, pair.fst)
|
||||
}
|
||||
|
||||
|
||||
// Applies a function to both elements of a Pair
|
||||
Problems.p6<A: Type, B: Type>(fn: A -> B, pair: Pair<A,A>): Pair<B,B>
|
||||
case pair {
|
||||
new : Pair.new!!(fn(pair.fst), fn(pair.snd))
|
||||
}
|
||||
|
||||
|
||||
// Doubles a number
|
||||
Problems.p7(n: Nat): Nat
|
||||
case n {
|
||||
zero: 0
|
||||
succ: Nat.succ(Nat.succ(Problems.p7(n.pred)))
|
||||
}
|
||||
|
||||
|
||||
// Halves a number, rounding down
|
||||
Problems.p8(n: Nat): Nat
|
||||
case n {
|
||||
zero: Nat.zero
|
||||
succ: case n.pred {
|
||||
zero: Nat.zero
|
||||
succ: Nat.succ(Problems.p8(n.pred.pred))
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// Adds two numbers
|
||||
Problems.p9(a: Nat, b: Nat): Nat
|
||||
case a {
|
||||
zero: b
|
||||
succ : Nat.succ(Problems.p9(a.pred, b))
|
||||
}
|
||||
|
||||
|
||||
// Subtracts two numbers
|
||||
Problems.p10(a: Nat, b: Nat): Nat
|
||||
case b {
|
||||
zero: a
|
||||
succ : case a {
|
||||
zero : 0
|
||||
succ : Problems.p10(a.pred, b.pred)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// Multiplies two numbers
|
||||
Problems.p11(a: Nat, b: Nat): Nat
|
||||
case a {
|
||||
zero : 0
|
||||
succ : Problems.p9(Problems.p11(a.pred, b), b)
|
||||
}
|
||||
|
||||
|
||||
// Returns true if a < b
|
||||
Problems.p12(a: Nat, b: Nat): Bool
|
||||
case Nat.sub(a,b){
|
||||
zero: case Problems.p10(b,a){
|
||||
zero: true
|
||||
succ: true
|
||||
}
|
||||
succ: case Problems.p10(b,a){
|
||||
zero: false
|
||||
succ: false
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// Returns true if a == b
|
||||
Problems.p13(a: Nat, b: Nat): Bool
|
||||
case a {
|
||||
zero: case b {
|
||||
zero:
|
||||
case Nat.sub(a,b){
|
||||
zero: true
|
||||
succ: false
|
||||
}
|
||||
succ:
|
||||
case Nat.sub(b,a){
|
||||
zero: true
|
||||
succ: false
|
||||
}
|
||||
}
|
||||
succ: case b {
|
||||
zero:
|
||||
case Nat.sub(a,b){
|
||||
zero: true
|
||||
succ: false
|
||||
}
|
||||
succ:
|
||||
case Nat.sub(b,a){
|
||||
zero: true
|
||||
succ: false
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// Returns the first element of a List
|
||||
Problems.p14<A: Type>(xs: List<A>): Maybe<A>
|
||||
case xs {
|
||||
nil: none
|
||||
cons: some(xs.head)
|
||||
}
|
||||
|
||||
|
||||
// Returns the list without the first element
|
||||
Problems.p15<A: Type>(xs: List<A>): List<A>
|
||||
case xs {
|
||||
nil: []
|
||||
cons: xs.tail
|
||||
}
|
||||
|
||||
|
||||
Problems.p16<A: Type>(xs: List<A>): Nat
|
||||
case xs {
|
||||
nil: 0
|
||||
cons: Nat.succ(Problems.p16!(xs.tail))
|
||||
}
|
||||
|
||||
|
||||
// Concatenates two lists
|
||||
Problems.p17<A: Type>(xs: List<A>, ys: List<A>): List<A>
|
||||
case xs {
|
||||
nil : ys
|
||||
cons : xs.head & Problems.p17!(xs.tail, ys)
|
||||
}
|
||||
|
||||
|
||||
// Applies a function to all elements of a list
|
||||
Problems.p18<A: Type, B: Type>(fn: A -> B, xs: List<A>): List<B>
|
||||
case xs {
|
||||
nil: []
|
||||
cons : fn(xs.head) & Problems.p18!!(fn, xs.tail)
|
||||
}
|
||||
|
||||
|
||||
// Returns the same list, with the order reversed
|
||||
Problems.p19<A: Type>(xs: List<A>): List<A>
|
||||
case xs {
|
||||
nil: []
|
||||
cons : Problems.p17!(Problems.p19!(xs.tail), List.cons!(xs.head, List.nil!))
|
||||
}
|
||||
|
||||
|
||||
// Returns pairs of the elements of the 2 input lists on the same index
|
||||
Problems.p20<A: Type, B: Type>(xs: List<A>, ys: List<B>): List<Pair<A,B>>
|
||||
case xs ys {
|
||||
cons cons : List.cons<Pair<A,B>>(Pair.new!!(xs.head, ys.head), Problems.p20!!(xs.tail, ys.tail))
|
||||
} default []
|
||||
|
||||
|
||||
// Returns the smallest element of a List
|
||||
Problems.p21(xs: List<Nat>): Nat
|
||||
case xs {
|
||||
nil : 0
|
||||
cons :
|
||||
case xs.tail {
|
||||
nil: xs.head
|
||||
cons:
|
||||
let min = Problems.p21(xs.tail)
|
||||
Problems.p21_sup(xs.head, min)
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
Problems.p21_sup(a: Nat, b: Nat): Nat
|
||||
case Problems.p12(a,b) {
|
||||
true: a
|
||||
false: b
|
||||
}
|
||||
|
||||
|
||||
// Returns the same list without the smallest element
|
||||
Problems.p22(xs: List<Nat>): List<Nat>
|
||||
case xs {
|
||||
nil: []
|
||||
cons:
|
||||
let min = Problems.p22_menor(xs.head, xs.tail)
|
||||
Problems.p22_remover([], min, xs)
|
||||
}
|
||||
|
||||
Problems.p22_remover(i: List<Nat>, j: Nat, xs: List<Nat>): List<Nat>
|
||||
case xs {
|
||||
nil: Problems.p19!(i)
|
||||
cons:
|
||||
case Nat.eql(j, xs.head) {
|
||||
true: Problems.p17!(Problems.p19!(i), xs.tail)
|
||||
false: Problems.p22_remover(List.cons!(xs.head, i), j, xs.tail)
|
||||
}
|
||||
}
|
||||
|
||||
Problems.p22_menor(x: Nat, xs: List<Nat>): Nat
|
||||
case xs {
|
||||
nil: x
|
||||
cons:
|
||||
case Problems.p22_lte(x, xs.head) {
|
||||
true: Problems.p22_menor(x, xs.tail)
|
||||
false: Problems.p22_menor(xs.head, xs.tail)
|
||||
}
|
||||
}
|
||||
|
||||
Problems.p22_lte(a: Nat, b: Nat): Bool
|
||||
case Problems.p10(a,b){
|
||||
zero: case Problems.p10(b,a){
|
||||
zero: true
|
||||
succ: true
|
||||
}
|
||||
succ: case Problems.p10(b,a){
|
||||
zero: true
|
||||
succ: false
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// Returns the same list, in ascending order
|
||||
//Problems.p23(xs: List<Nat>): List<Nat>
|
||||
// ?a
|
||||
|
||||
// -----------------------------------------------------------------------------
|
||||
|
||||
// ::::::::::::::
|
||||
// :: Theorems ::
|
||||
// ::::::::::::::
|
||||
|
||||
// Note: these problems use functions from the base libs, NOT the ones above
|
||||
|
||||
Problems.t0: true == true
|
||||
refl
|
||||
|
||||
|
||||
Problems.t1(a: Bool): Bool.and(false, a) == false
|
||||
refl
|
||||
|
||||
|
||||
Problems.t2(a: Bool): Bool.and(a, false) == false
|
||||
case a {
|
||||
true: refl
|
||||
false: refl
|
||||
}!
|
||||
|
||||
|
||||
Problems.t3(a: Bool): Bool.or(true, a) == true
|
||||
refl
|
||||
|
||||
|
||||
Problems.t4(a: Bool): Bool.or(a, true) == true
|
||||
case a {
|
||||
true: refl
|
||||
false: refl
|
||||
}!
|
||||
|
||||
|
||||
Problems.t5(a: Bool): Bool.eql(a, a) == true
|
||||
case a {
|
||||
true: refl
|
||||
false: refl
|
||||
}!
|
||||
|
||||
|
||||
Problems.t6(a: Bool): Bool.not(Bool.not(a)) == a
|
||||
case a {
|
||||
true: refl
|
||||
false: refl
|
||||
}!
|
||||
|
||||
|
||||
Problems.t7(a: Bool, b: Bool): Bool.not(Bool.and(a,b)) == Bool.or(Bool.not(a), Bool.not(b))
|
||||
case a b {
|
||||
true true: refl
|
||||
true false: refl
|
||||
false true: refl
|
||||
false false: refl
|
||||
}!
|
||||
|
||||
|
||||
Problems.t8(a: Bool, b: Bool): Bool.not(Bool.or(a,b)) == Bool.and(Bool.not(a), Bool.not(b))
|
||||
case a b {
|
||||
true true: refl
|
||||
true false: refl
|
||||
false true: refl
|
||||
false false: refl
|
||||
}!
|
||||
|
||||
|
||||
Problems.t9(a: Pair<Nat,Nat>): Pair.new<Nat,Nat>(Pair.fst<Nat,Nat>(a), Pair.snd<Nat,Nat>(a)) == a
|
||||
case a {
|
||||
new: refl
|
||||
}!
|
||||
|
||||
|
||||
Problems.t10(a: Pair<Nat,Nat>): Pair.swap<Nat,Nat>(Pair.swap<Nat,Nat>(a)) == a
|
||||
case a {
|
||||
new: refl
|
||||
}!
|
||||
|
||||
|
||||
Problems.t11(n: Nat): Nat.same(n) == n
|
||||
case n {
|
||||
zero: refl
|
||||
succ: apply(Nat.succ, Problems.t11(n.pred))
|
||||
}!
|
||||
|
||||
|
||||
Problems.t12(n: Nat): Nat.half(Nat.double(n)) == n
|
||||
case n {
|
||||
zero: refl
|
||||
succ: apply(Nat.succ, Problems.t12(n.pred))
|
||||
}!
|
||||
|
||||
|
||||
Problems.t13(n: Nat): Nat.add(0,n) == n
|
||||
refl
|
||||
|
||||
Problems.t14(n: Nat): Nat.add(n,0) == n
|
||||
case n {
|
||||
zero: refl
|
||||
succ: apply(Nat.succ, Problems.t14(n.pred))
|
||||
}!
|
||||
|
||||
|
||||
Problems.t15(n: Nat, m: Nat): Nat.add(Nat.succ(n),m) == Nat.succ(Nat.add(n,m))
|
||||
refl
|
||||
|
||||
Problems.t16(n: Nat, m: Nat): Nat.add(n,Nat.succ(m)) == Nat.succ(Nat.add(n,m))
|
||||
case n {
|
||||
zero: refl
|
||||
succ: apply(Nat.succ, Problems.t16(n.pred, m))
|
||||
}!
|
||||
|
||||
Problems.t17(n: Nat, m: Nat): Nat.add(n,m) == Nat.add(m,n)
|
||||
case n {
|
||||
zero: mirror(Problems.t14(m))
|
||||
succ:
|
||||
let ind = Problems.t17(n.pred, m)
|
||||
let app = apply(Nat.succ, ind)
|
||||
let first = mirror(Problems.t16(m, n.pred ))
|
||||
let ok = Equal.chain!!!!(app, first)
|
||||
ok
|
||||
}!
|
||||
|
||||
Problems.t18(n: Nat): Nat.add(n,n) == Nat.double(n)
|
||||
case n{
|
||||
zero: refl
|
||||
succ:
|
||||
let ind = Problems.t18(n.pred)
|
||||
let app = apply(Nat.succ, ind)
|
||||
let first = Problems.t16(n.pred,n.pred)
|
||||
let ok = Equal.chain!!!!(first, app)
|
||||
apply(Nat.succ, ok)
|
||||
}!
|
||||
|
||||
|
||||
Problems.t19(n: Nat): Nat.ltn(n, Nat.succ(n)) == true
|
||||
case n {
|
||||
zero: refl
|
||||
succ: Problems.t19(n.pred)
|
||||
}!
|
||||
|
||||
|
||||
Problems.t20(n: Nat): Nat.gtn(Nat.succ(n), n) == true
|
||||
case n {
|
||||
zero: refl
|
||||
succ: Problems.t20(n.pred)
|
||||
}!
|
||||
|
||||
|
||||
Problems.t21(n: Nat): Nat.sub(n,n) == 0
|
||||
case n {
|
||||
zero: refl
|
||||
succ: Problems.t21(n.pred)
|
||||
}!
|
||||
|
||||
|
||||
Problems.t22(n: Nat, e: n == 1): Nat.succ(n) == 2
|
||||
apply(Nat.succ, e)
|
||||
|
||||
|
||||
//Problems.t23(n: Nat, m: Nat, e: Nat.eql(n,m) == true): n == m
|
||||
// ?a
|
||||
|
||||
|
||||
Problems.t24(xs: List<Nat>): Nat.gtn(List.length<Nat>(List.cons<Nat>(1,xs)),0) == true
|
||||
refl
|
||||
|
||||
|
||||
Problems.t25(xs: List<Nat>): List.map<Nat,Nat>((x) x, xs) == xs
|
||||
case xs {
|
||||
nil: refl
|
||||
cons: apply(List.cons<Nat>(xs.head), Problems.t25(xs.tail))
|
||||
}!
|
||||
|
||||
|
||||
Problems.t26(xs: List<Nat>, ys: List<Nat>): Nat.add(List.length<Nat>(xs), List.length<Nat>(ys)) == List.length<Nat>(List.concat<Nat>(xs,ys))
|
||||
case xs {
|
||||
nil: refl
|
||||
cons: apply(Nat.succ, Problems.t26(xs.tail, ys))
|
||||
}!
|
||||
|
||||
|
||||
//Problems.t27(xs: List<Nat>): List.reverse<Nat>(List.reverse<Nat>(xs)) == xs
|
||||
// ?a
|
||||
|
||||
|
||||
//Problems.t28: true != false
|
||||
// ?a
|
||||
|
||||
|
||||
//Problems.t29: 3 != 2
|
||||
// ?a
|
||||
|
||||
|
||||
//Problems.t30(a: Bool): Bool.or(true, a) != false
|
||||
// ?a
|
||||
|
||||
|
||||
//Problems.t31(a: Bool): Bool.or(a, true) != false
|
||||
// ?a
|
||||
|
||||
|
||||
//Problems.t32(a: Bool): Bool.and(false, a) != true
|
||||
// ?a
|
||||
|
||||
|
||||
//Problems.t33(a: Bool): Bool.and(a, false) != true
|
||||
// ?a
|
||||
|
||||
|
||||
Problems.t34(a: Nat, b: Nat, e: a == b): b == a
|
||||
case e {
|
||||
refl: refl
|
||||
}!
|
||||
|
||||
|
||||
Problems.t35(a: Nat, b: Nat, c: Nat, e0: a == b, e1: b == c): a == c
|
||||
Equal.chain!!!!(e0, e1)
|
||||
|
||||
|
||||
//Problems.t36(a: Nat, P: Nat -> Type, p: P(a)): P(Nat.same(a))
|
||||
// ?a
|
@ -24,6 +24,7 @@ var server_apps = [
|
||||
'Ludo.kind',
|
||||
'Playground.kind',
|
||||
'Pong.kind',
|
||||
'RLP.kind',
|
||||
'Seta.kind',
|
||||
'TicTacToe.kind'
|
||||
]
|
||||
|
Loading…
Reference in New Issue
Block a user